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 A4, A5, GROUP_2:50, GROUP_6:def 6;
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 A8, STRUCT_0:def 5;
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 A7, Def18;
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 A10, Lm13, GROUP_2:51;
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 A13, STRUCT_0:def 5;
dom f = the carrier of G by FUNCT_2:def 1;
then [g,h] in f by A12, FUNCT_1:1;
hence h in f .: the carrier of G9 by A14, RELSET_1:29; :: 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 A15, FUNCT_1:1, STRUCT_0:def 5;
hence h in A ; :: thesis: verum

end;

hence the carrier of H99 = f .: the carrier of G9 by A11, SUBSET_1:3; :: thesis: verum