let G, H be Group; :: thesis: for K being Subgroup of H
for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K
let K be Subgroup of H; :: thesis: for f being Homomorphism of G,H ex J being strict Subgroup of G st the carrier of J = f " the carrier of K
let f be Homomorphism of G,H; :: thesis: ex J being strict Subgroup of G st the carrier of J = f " the carrier of K
f . (1_ G) = 1_ H by GROUP_6:31;
then f . (1_ G) in K by GROUP_2:46;
then reconsider Ivf = f " the carrier of K as non empty Subset of the carrier of G by FUNCT_2:38;
D191: for g1, g2 being Element of G st g1 in Ivf & g2 in Ivf holds
g1 * g2 in Ivf

proof

let g1, g2 be Element of G; :: thesis: ( g1 in Ivf & g2 in Ivf implies g1 * g2 in Ivf )
D94: f . (g1 * g2) = (f . g1) * (f . g2) by GROUP_6:def 6;
assume ( g1 in Ivf & g2 in Ivf ) ; :: thesis: g1 * g2 in Ivf
then ( f . g1 in K & f . g2 in K ) by FUNCT_2:38;
then (f . g1) * (f . g2) in K by GROUP_2:50;
hence g1 * g2 in Ivf by D94, FUNCT_2:38; :: thesis: verum

end;

for g being Element of G st g in Ivf holds
g " in Ivf

proof

let g be Element of G; :: thesis: ( g in Ivf implies g " in Ivf )
assume g in Ivf ; :: thesis: g " in Ivf
then f . g in K by FUNCT_2:38;
then (f . g) " in K by GROUP_2:51;
then f . (g ") in the carrier of K by GROUP_6:32;
hence g " in Ivf by FUNCT_2:38; :: thesis: verum

end;

then consider J being strict Subgroup of G such that
D19: the carrier of J = f " the carrier of K by GROUP_2:52, D191;
take J ; :: thesis: the carrier of J = f " the carrier of K
thus the carrier of J = f " the carrier of K by D19; :: thesis: verum