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

g " in Ivf

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

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

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

g " in Ivf

proof

then consider J being strict Subgroup of G such that
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;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

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