let O be set ; :: thesis: for G being GroupWithOperators of O
for H being strict GroupWithOperators of O
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let G be GroupWithOperators of O; :: thesis: for H being strict GroupWithOperators of O
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )
let H be strict GroupWithOperators of O; :: 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

reconsider H9 = H as strict StableSubgroup of H by Lm3;
assume rng h = the carrier of H ; :: according to FUNCT_2:def 3 :: thesis: Image h = H
then the carrier of H9 = the carrier of (Image h) by Th49;
hence Image h = H by Lm4; :: 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, Def22;
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 by XBOOLE_0:def 10;
hence h is onto ; :: thesis: verum