let G be Group; :: thesis: for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let H be strict Group; :: thesis: for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let h be Homomorphism of G,H; :: thesis: ( h is onto iff Image h = H )
thus ( h is onto implies Image h = H ) :: thesis: ( Image h = H implies h is onto )

proof

assume rng h = the carrier of H ; :: according to FUNCT_2:def 3 :: thesis: Image h = H
then the carrier of (Image h) = the carrier of H by Th44;
hence Image h = H by GROUP_2:61; :: thesis: verum

end;

assume A1: Image h = H ; :: thesis: h is onto
the carrier of H c= rng h

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of H or x in rng h )
assume x in the carrier of H ; :: thesis: x in rng h
then x in h .: the carrier of G by A1, Def10;
then ex y being object st
( y in dom h & y in the carrier of G & h . y = x ) by FUNCT_1:def 6;
hence x in rng h by FUNCT_1:def 3; :: thesis: verum

end;

then rng h = the carrier of H ;
hence h is onto ; :: thesis: verum