Proof if $g$ is surjective, then $g\circ f=I_X$. 
Let $X$ and $Y$ be nonempty sets, let $f:X→Y$ be a function, and let $g:Y→X$ be such that $f\circ g=I_Y$. Prove that if $g$ is surjective, then $g\circ f=I_X$.
$I_X:X \to X$ and $I_Y: Y \to Y$ are identity functions.


Let $x \in X$ be random.
Using composition definition, we get $(g \circ f)(x) = g(f(x))$.
Since $f(x)=y$, then $g(f(x))=g(y)$
Assuming $g$ is surjective, therefore for all $x \in X$ we have a $y \in Y$, such that $x=g(y)$.
Therefore $g(y)=x$ and $(g \circ f)(x) = g(f(x))=g(y)=x$
Since $g \circ f: X\to X$ and $I_X:X\to X$ and for all $x\in X$, $I_X(x)=(g\circ f)(x)=x$, we can conclude that $g\circ f=I_X$

Have I done this correctly?
 A: 
Let $x \in X$ be random.

Do not use the term "random" unless you're dealing with probability. It has a precise meaning. Instead, say "Consider some arbitrary $x \in X$."

Assuming $g$ is surjective,

We should assume $g$ is surjective before taking our arbitrary $x$ if we're being extremely formal.

therefore for all $x \in X$ we have a $y \in Y$, such that $x = g(y)$

You've just introduced a new bound variable $x$ which is different from the variable $x$ that you introduced earlier.

Therefore $g(y) = x$

We have not picked any specific $y$ such that $g(y) = x$. We have only asserted that $\forall x \in X \exists y \in Y (x = g(y))$.
The more precise way to prove this is:
Suppose $g$ is surjective. We wish to show that $g \circ f = I_X$; by function extensionality, it suffices to show that for all $x \in X$, $(g \circ f)(x) = I_X(x)$.
Now consider an arbitrary $x \in X$. Since we assumed $g$ is surjective, we can take some $y \in Y$ such that $x = g(y)$. Then we see that
$\begin{equation}
\begin{split}
(g \circ f)(x) &= g(f(x)) \\
&= g(f(g(y))) \\
&= g((f \circ g)(y)) \\
&= g(I_Y(y)) \\
&= g(y) \\
&= x \\
&= I_X(x)
\end{split}
\end{equation}$
which is the very thing we sought to show. $\square$
