let G1, G2 be Group; :: thesis: for H being Subgroup of G2
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G1,H st f1 = f2 holds
Image f1 = Image f2
let H be Subgroup of G2; :: thesis: for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G1,H st f1 = f2 holds
Image f1 = Image f2
let f1 be Homomorphism of G1,G2; :: thesis: for f2 being Homomorphism of G1,H st f1 = f2 holds
Image f1 = Image f2
let f2 be Homomorphism of G1,H; :: thesis: ( f1 = f2 implies Image f1 = Image f2 )
assume A1: f1 = f2 ; :: thesis: Image f1 = Image f2
A2: Image f2 is strict Subgroup of G2 by GROUP_2:56;
for g being Element of G2 holds
( g in Image f1 iff g in Image f2 )

proof

let g be Element of G2; :: thesis: ( g in Image f1 iff g in Image f2 )

hereby :: thesis: ( g in Image f2 implies g in Image f1 )

assume g in Image f1 ; :: thesis: g in Image f2
then ex a being Element of G1 st g = f1 . a by GROUP_6:45;
hence g in Image f2 by A1, GROUP_6:45; :: thesis: verum

end;

assume g in Image f2 ; :: thesis: g in Image f1
then ex a being Element of G1 st g = f2 . a by GROUP_6:45;
hence g in Image f1 by A1, GROUP_6:45; :: thesis: verum

end;

hence Image f1 = Image f2 by A2, GROUP_2:def 6; :: thesis: verum