let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ;
now :: thesis: for x being object st x in A holds
x in the carrier of H
let x be object ; :: thesis: ( x in A implies x in the carrier of H )
assume x in A ; :: thesis: x in the carrier of H
then ex g being Element of G st
( x = f . g & g in G99 ) ;
hence x in the carrier of H ; :: thesis: verum
end;
then reconsider A = A as Subset of H by TARSKI:def 3;
A1: now :: thesis: for h1, h2 being Element of H st h1 in A & h2 in A holds
h1 * h2 in A
let h1, h2 be Element of H; :: thesis: ( h1 in A & h2 in A implies h1 * h2 in A )
assume that
A2: h1 in A and
A3: h2 in A ; :: thesis: h1 * h2 in A
consider a being Element of G such that
A4: ( h1 = f . a & a in G99 ) by A2;
consider b being Element of G such that
A5: ( h2 = f . b & b in G99 ) by A3;
( f . (a * b) = h1 * h2 & a * b in G99 ) by ;
hence h1 * h2 in A ; :: thesis: verum
end;
A6: now :: thesis: for o being Element of O
for h being Element of H st h in A holds
(H ^ o) . h in A
let o be Element of O; :: thesis: for h being Element of H st h in A holds
(H ^ o) . h in A

let h be Element of H; :: thesis: ( h in A implies (H ^ o) . h in A )
assume h in A ; :: thesis: (H ^ o) . h in A
then consider g being Element of G such that
A7: h = f . g and
A8: g in G99 ;
g in the carrier of G99 by ;
then g in G9 by STRUCT_0:def 5;
then (G ^ o) . g in G9 by Lm9;
then (G ^ o) . g in the carrier of G9 by STRUCT_0:def 5;
then A9: (G ^ o) . g in G99 by STRUCT_0:def 5;
(H ^ o) . h = f . ((G ^ o) . g) by ;
hence (H ^ o) . h in A by A9; :: thesis: verum
end;
now :: thesis: for h being Element of H st h in A holds
h " in A
let h be Element of H; :: thesis: ( h in A implies h " in A )
assume h in A ; :: thesis: h " in A
then consider g being Element of G such that
A10: ( h = f . g & g in G99 ) ;
( g " in G99 & h " = f . (g ") ) by ;
hence h " in A ; :: thesis: verum
end;
then consider H99 being strict StableSubgroup of H such that
A11: the carrier of H99 = A by A1, A6, Lm14;
take H99 ; :: thesis: the carrier of H99 = f .: the carrier of G9
now :: thesis: for h being Element of H holds
( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )
set R = f;
let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G9 ) & ( h in f .: the carrier of G9 implies h in A ) )
reconsider R = f as Relation of the carrier of G, the carrier of H ;
hereby :: thesis: ( h in f .: the carrier of G9 implies h in A )
assume h in A ; :: thesis: h in f .: the carrier of G9
then consider g being Element of G such that
A12: h = f . g and
A13: g in G99 ;
A14: g in the carrier of G9 by ;
dom f = the carrier of G by FUNCT_2:def 1;
then [g,h] in f by ;
hence h in f .: the carrier of G9 by ; :: thesis: verum
end;
assume h in f .: the carrier of G9 ; :: thesis: h in A
then consider g being Element of G such that
A15: ( [g,h] in R & g in the carrier of G9 ) by RELSET_1:29;
( f . g = h & g in G99 ) by ;
hence h in A ; :: thesis: verum
end;
hence the carrier of H99 = f .: the carrier of G9 by ; :: thesis: verum