Trouble understanding surjective function proof

Question

I'm studying for my discrete math exam and I'm having some trouble understanding this practice problem and solution. I know what surjective functions are, but I can't really understand the way this trait is proved in this example, especially the purpose of the ending exist statement. Could someone translate the steps to plain English for me?

3. Let f:A->B be a function. Show, by direct inference, that 
       (Exist g:B->A, All y in B, f.g(y) = y) => (f is surjective)

Sol:
 y in B
=> {All y in B, f.g(y) = y}
 f.g(y) = y
=> {Definition of "."}
 f(g(y)) = y
=> {Let x be the element g(y) in A}
 Exist x in A, f(x) = y

Thanks.

Answer 1

Suppose $f:A\to B$, and suppose that $g:B\to A$ is such that for all $y\in B$, $f(g(y)) = y$. We want to show $f$ is surjective. So choose $y\in B$, and consider $g(y)\in A$. Since $f(g(y)) = y$ by hypothesis, $g(y)$ is an element of $A$ whose image is $y$, so that $f$ is surjective.

Answer 2

Rather plain english:

We have $f:A\rightarrow B$ and $g:B\rightarrow A$ with the property that for any $y \in B,$ $(f\circ g)(y) = y$ holds. Recall that $(f\circ g)(y) = f(g(y)),$ that's just notation.

Now we want to show that $f$ is surjective. To this end, we pick an arbitrary $y \in B$ and have to produce an $x\in A$ such that $f(x) = y.$ But since we have $g$ with the special property, thats quite easy. We just put $x := g(y) \in A$ and verify $f(x) = f(g(y)) = y,$ as desired.