let X, Y be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )
let f be Function of X,Y; :: thesis: for g being Function of Y,X st g * f = id X holds
( f is one-to-one & g is onto )
let g be Function of Y,X; :: thesis: ( g * f = id X implies ( f is one-to-one & g is onto ) )
assume A1: g * f = id X ; :: thesis: ( f is one-to-one & g is onto )
thus f is one-to-one :: thesis: g is onto

proof

per cases ( Y = {} or Y <> {} ) ;

suppose Y = {} ; :: thesis: f is one-to-one

hence f is one-to-one ; :: thesis: verum

end;

suppose Y <> {} ; :: thesis: f is one-to-one

then dom f = X by Def1;
hence f is one-to-one by A1, FUNCT_1:31; :: thesis: verum

end;

end;

end;

rng (g * f) = X by A1;
then X c= rng g by RELAT_1:26;
hence rng g = X ; :: according to FUNCT_2:def 3 :: thesis: verum