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 )

the carrier of H c= rng h

hence h is onto ; :: thesis: verum

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

assume A1:
Image h = H
; :: thesis: h is onto
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 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

the carrier of H c= rng h

proof

then
rng h = the carrier of H
by XBOOLE_0:def 10;
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;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

hence h is onto ; :: thesis: verum