let X, Y be non empty set ; :: thesis: for f being Function of X,Y st f is onto holds
ex g being Function of Y,X st f * g = id Y
let f be Function of X,Y; :: thesis: ( f is onto implies ex g being Function of Y,X st f * g = id Y )
assume A1: f is onto ; :: thesis: ex g being Function of Y,X st f * g = id Y
defpred S₁[ object , object ] means $1 = f . $2;
A2: for y being object st y in Y holds
ex x being object st
( x in X & S₁[y,x] )

proof

let y be object ; :: thesis: ( y in Y implies ex x being object st
( x in X & S₁[y,x] ) )
assume y in Y ; :: thesis: ex x being object st
( x in X & S₁[y,x] )
then reconsider yy = y as Element of Y ;
consider x being Element of X such that
B1: f . x = yy by A1, GROUP_6:58;
take x ; :: thesis: ( x in X & S₁[y,x] )
thus x in X ; :: thesis: S₁[y,x]
thus S₁[y,x] by B1; :: thesis: verum

end;

consider g being Function of Y,X such that
A3: for y being object st y in Y holds
S₁[y,g . y] from FUNCT_2:sch 1(A2);
take g ; :: thesis: f * g = id Y
for y being Element of Y holds (f * g) . y = y

proof

let y be Element of Y; :: thesis: (f * g) . y = y
B1: ( dom g = Y & dom (f * g) = dom g ) by FUNCT_2:123, FUNCT_2:def 1;
y = f . (g . y) by A3
.= (f * g) . y by B1, FUNCT_1:12 ;
hence (f * g) . y = y ; :: thesis: verum

end;

hence f * g = id Y by FUNCT_2:124; :: thesis: verum