let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2
for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2
let f be Homomorphism of G1,G2; :: thesis: for H2 being Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2
let H2 be Subgroup of G2; :: thesis: ex H1 being strict Subgroup of G1 st the carrier of H1 = f " the carrier of H2
A1: for g being Element of G1 st g in f " the carrier of H2 holds
g " in f " the carrier of H2

proof

let g be Element of G1; :: thesis: ( g in f " the carrier of H2 implies g " in f " the carrier of H2 )
assume g in f " the carrier of H2 ; :: thesis: g " in f " the carrier of H2
then f . g in the carrier of H2 by FUNCT_2:38;
then f . g in H2 by STRUCT_0:def 5;
then (f . g) " in H2 by GROUP_2:51;
then f . (g ") in H2 by GROUP_6:32;
then f . (g ") in the carrier of H2 by STRUCT_0:def 5;
hence g " in f " the carrier of H2 by FUNCT_2:38; :: thesis: verum

end;

A2: for g1, g2 being Element of G1 st g1 in f " the carrier of H2 & g2 in f " the carrier of H2 holds
g1 * g2 in f " the carrier of H2

proof

let g1, g2 be Element of G1; :: thesis: ( g1 in f " the carrier of H2 & g2 in f " the carrier of H2 implies g1 * g2 in f " the carrier of H2 )
assume that
A3: g1 in f " the carrier of H2 and
A4: g2 in f " the carrier of H2 ; :: thesis: g1 * g2 in f " the carrier of H2
f . g2 in the carrier of H2 by A4, FUNCT_2:38;
then A5: f . g2 in H2 by STRUCT_0:def 5;
f . g1 in the carrier of H2 by A3, FUNCT_2:38;
then f . g1 in H2 by STRUCT_0:def 5;
then (f . g1) * (f . g2) in H2 by A5, GROUP_2:50;
then f . (g1 * g2) in H2 by GROUP_6:def 6;
then f . (g1 * g2) in the carrier of H2 by STRUCT_0:def 5;
hence g1 * g2 in f " the carrier of H2 by FUNCT_2:38; :: thesis: verum

end;

1_ G2 in H2 by GROUP_2:46;
then 1_ G2 in the carrier of H2 by STRUCT_0:def 5;
then f . (1_ G1) in the carrier of H2 by GROUP_6:31;
then f " the carrier of H2 <> {} by FUNCT_2:38;
then consider H1 being strict Subgroup of G1 such that
A6: the carrier of H1 = f " the carrier of H2 by A1, A2, GROUP_2:52;
take H1 ; :: thesis: the carrier of H1 = f " the carrier of H2
thus the carrier of H1 = f " the carrier of H2 by A6; :: thesis: verum