let O be set ; for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9
let G, H be GroupWithOperators of O; for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9
let G9 be strict StableSubgroup of G; for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9
reconsider G99 = multMagma(# the carrier of G9, the multF of G9 #) as strict Subgroup of G by Lm15;
let f be Homomorphism of G,H; ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9
set A = { (f . g) where g is Element of G : g in G99 } ;
1_ G in G99
by GROUP_2:46;
then
f . (1_ G) in { (f . g) where g is Element of G : g in G99 }
;
then reconsider A = { (f . g) where g is Element of G : g in G99 } as non empty set ;
then reconsider A = A as Subset of H by TARSKI:def 3;
then consider H99 being strict StableSubgroup of H such that
A11:
the carrier of H99 = A
by A1, A6, Lm14;
take
H99
; the carrier of H99 = f .: the carrier of G9
hence
the carrier of H99 = f .: the carrier of G9
by A11, SUBSET_1:3; verum