There is the following problem:

> 
> Prove that a set $ G \neq \emptyset$, together with an associative binary operation $ \* $ on $ G $ such that $ a \* x = b $ and $ y \* a = b $ have solutions in $ G $ for any $ a,b \in G $, is a group.
> 
> 
> 

I looked at existing proofs and they all start with:

> 
> $ ax = a $ has a solution $ e $
> 
> 
> 

My question:   

How does one know this? In my eyes those proofs come up with unproven "facts" (or a hypotheses?) that serve as a base for the rest of the proof.

In this case assuming that ax = a even has a solution feels like skipping a part of the proof that may be intuitive for some, but I would like to have no such skips.

How can this be explained in more detail? Giving out the full proof with detailed explanations would be really appreciated!