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 for g being Element of G st g in Ivf holds
g " in Ivf 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