let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2
for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1
let f be Homomorphism of G1,G2; :: thesis: for H1 being Subgroup of G1 ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1
let H1 be Subgroup of G1; :: thesis: ex H2 being strict Subgroup of G2 st the carrier of H2 = f .: the carrier of H1
reconsider y = f . (1_ G1) as Element of G2 ;
A1: for g being Element of G2 st g in f .: the carrier of H1 holds
g " in f .: the carrier of H1

proof

let g be Element of G2; :: thesis: ( g in f .: the carrier of H1 implies g " in f .: the carrier of H1 )
assume g in f .: the carrier of H1 ; :: thesis: g " in f .: the carrier of H1
then consider x being Element of G1 such that
A2: x in the carrier of H1 and
A3: g = f . x by FUNCT_2:65;
x in H1 by A2, STRUCT_0:def 5;
then x " in H1 by GROUP_2:51;
then A4: x " in the carrier of H1 by STRUCT_0:def 5;
f . (x ") = (f . x) " by GROUP_6:32;
hence g " in f .: the carrier of H1 by A3, A4, FUNCT_2:35; :: thesis: verum

end;

A5: for g1, g2 being Element of G2 st g1 in f .: the carrier of H1 & g2 in f .: the carrier of H1 holds
g1 * g2 in f .: the carrier of H1

proof

let g1, g2 be Element of G2; :: thesis: ( g1 in f .: the carrier of H1 & g2 in f .: the carrier of H1 implies g1 * g2 in f .: the carrier of H1 )
assume that
A6: g1 in f .: the carrier of H1 and
A7: g2 in f .: the carrier of H1 ; :: thesis: g1 * g2 in f .: the carrier of H1
consider x being Element of G1 such that
A8: x in the carrier of H1 and
A9: g1 = f . x by A6, FUNCT_2:65;
consider y being Element of G1 such that
A10: y in the carrier of H1 and
A11: g2 = f . y by A7, FUNCT_2:65;
A12: y in H1 by A10, STRUCT_0:def 5;
x in H1 by A8, STRUCT_0:def 5;
then x * y in H1 by A12, GROUP_2:50;
then A13: x * y in the carrier of H1 by STRUCT_0:def 5;
f . (x * y) = (f . x) * (f . y) by GROUP_6:def 6;
hence g1 * g2 in f .: the carrier of H1 by A9, A11, A13, FUNCT_2:35; :: thesis: verum

end;

1_ G1 in H1 by GROUP_2:46;
then ( dom f = the carrier of G1 & 1_ G1 in the carrier of H1 ) by FUNCT_2:def 1, STRUCT_0:def 5;
then y in f .: the carrier of H1 by FUNCT_1:def 6;
then consider H2 being strict Subgroup of G2 such that
A14: the carrier of H2 = f .: the carrier of H1 by A1, A5, GROUP_2:52;
take H2 ; :: thesis: the carrier of H2 = f .: the carrier of H1
thus the carrier of H2 = f .: the carrier of H1 by A14; :: thesis: verum