let O be set ; :: thesis: for G, H being GroupWithOperators of O
for G' being strict StableSubgroup of G
for f being Homomorphism of G,H ex H' being strict StableSubgroup of H st the carrier of H' = f .: the carrier of G'
let G, H be GroupWithOperators of O; :: thesis: for G' being strict StableSubgroup of G
for f being Homomorphism of G,H ex H' being strict StableSubgroup of H st the carrier of H' = f .: the carrier of G'
let G' be strict StableSubgroup of G; :: thesis: for f being Homomorphism of G,H ex H' being strict StableSubgroup of H st the carrier of H' = f .: the carrier of G'
let f be Homomorphism of G,H; :: thesis: ex H' being strict StableSubgroup of H st the carrier of H' = f .: the carrier of G'
reconsider G'' = multMagma(# the carrier of G',the multF of G' #) as strict Subgroup of G by Lm16;
set A = { (f . g) where g is Element of G : g in G'' } ;
1_ G in G'' by GROUP_2:55;
then f . (1_ G) in { (f . g) where g is Element of G : g in G'' } ;
then reconsider A = { (f . g) where g is Element of G : g in G'' } as non empty set ;

now

let x be set ; :: thesis: ( x in A implies x in the carrier of H )
assume x in A ; :: thesis: x in the carrier of H
then consider g being Element of G such that
A1: ( x = f . g & g in G'' ) ;
thus x in the carrier of H by A1; :: thesis: verum

end;

then reconsider A = A as Subset of H by TARSKI:def 3;

A2: now

let h1, h2 be Element of H; :: thesis: ( h1 in A & h2 in A implies h1 * h2 in A )
assume A3: ( h1 in A & h2 in A ) ; :: thesis: h1 * h2 in A
then consider a being Element of G such that
A4: ( h1 = f . a & a in G'' ) ;
consider b being Element of G such that
A5: ( h2 = f . b & b in G'' ) by A3;
A6: f . (a * b) = h1 * h2 by A4, A5, GROUP_6:def 7;
a * b in G'' by A4, A5, GROUP_2:59;
hence h1 * h2 in A by A6; :: thesis: verum

end;

A7: now

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
A8: ( h = f . g & g in G'' ) ;
A9: g " in G'' by A8, GROUP_2:60;
h " = f . (g " ) by A8, Lm14;
hence h " in A by A9; :: thesis: verum

end;

now

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
A10: ( h = f . g & g in G'' ) ;
A11: (H ^ o) . h = f . ((G ^ o) . g) by A10, Def18;
g in the carrier of G'' by A10, STRUCT_0:def 5;
then g in G' by STRUCT_0:def 5;
then (G ^ o) . g in G' by Lm10;
then (G ^ o) . g in the carrier of G' by STRUCT_0:def 5;
then (G ^ o) . g in G'' by STRUCT_0:def 5;
hence (H ^ o) . h in A by A11; :: thesis: verum

end;

then consider H'' being strict StableSubgroup of H such that
A12: the carrier of H'' = A by A2, A7, Lm15;
take H'' ; :: thesis: the carrier of H'' = f .: the carrier of G'

now

let h be Element of H; :: thesis: ( ( h in A implies h in f .: the carrier of G' ) & ( h in f .: the carrier of G' implies h in A ) )
set R = f;
reconsider R = f as Relation of the carrier of G,the carrier of H ;

hereby :: thesis: ( h in f .: the carrier of G' implies h in A )

assume h in A ; :: thesis: h in f .: the carrier of G'
then consider g being Element of G such that
A13: ( h = f . g & g in G'' ) ;
dom f = the carrier of G by FUNCT_2:def 1;
then A14: [g,h] in f by A13, FUNCT_1:8;
g in the carrier of G' by A13, STRUCT_0:def 5;
hence h in f .: the carrier of G' by A14, RELSET_1:52; :: thesis: verum

end;

assume h in f .: the carrier of G' ; :: thesis: h in A
then consider g being Element of G such that
A15: ( [g,h] in R & g in the carrier of G' ) by RELSET_1:52;
A16: f . g = h by A15, FUNCT_1:8;
g in G'' by A15, STRUCT_0:def 5;
hence h in A by A16; :: thesis: verum

end;

hence the carrier of H'' = f .: the carrier of G' by A12, SUBSET_1:8; :: thesis: verum