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
A1: dom f = the carrier of G1 by FUNCT_2:def 1;
1_ G1 in H1 by GROUP_2:55;
then A2: 1_ G1 in the carrier of H1 by STRUCT_0:def 5;
reconsider y = f . (1_ G1) as Element of G2 ;
A3: y in f .: the carrier of H1 by A1, A2, FUNCT_1:def 12;
A4: 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
A5: ( x in the carrier of H1 & g = f . x ) by FUNCT_2:116;
x in H1 by A5, STRUCT_0:def 5;
then x " in H1 by GROUP_2:60;
then A6: x " in the carrier of H1 by STRUCT_0:def 5;
f . (x " ) = (f . x) " by GROUP_6:41;
hence g " in f .: the carrier of H1 by A5, A6, FUNCT_2:43; :: thesis: verum

end;

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 A7: ( g1 in f .: the carrier of H1 & g2 in f .: the carrier of H1 ) ; :: thesis: g1 * g2 in f .: the carrier of H1
then consider x being Element of G1 such that
A8: ( x in the carrier of H1 & g1 = f . x ) by FUNCT_2:116;
A9: x in H1 by A8, STRUCT_0:def 5;
consider y being Element of G1 such that
A10: ( y in the carrier of H1 & g2 = f . y ) by A7, FUNCT_2:116;
y in H1 by A10, STRUCT_0:def 5;
then x * y in H1 by A9, GROUP_2:59;
then A11: x * y in the carrier of H1 by STRUCT_0:def 5;
f . (x * y) = (f . x) * (f . y) by GROUP_6:def 7;
hence g1 * g2 in f .: the carrier of H1 by A8, A10, A11, FUNCT_2:43; :: thesis: verum

end;

then consider H2 being strict Subgroup of G2 such that
A12: the carrier of H2 = f .: the carrier of H1 by A3, A4, GROUP_2:61;
take H2 ; :: thesis: the carrier of H2 = f .: the carrier of H1
thus the carrier of H2 = f .: the carrier of H1 by A12; :: thesis: verum