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'
reconsider G'' = multMagma(# the carrier of G',the multF of G' #) as strict Subgroup of G by Lm16;
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'
set A = { (f . g) where g is Element of : g in G'' } ;
1_ G in G'' by GROUP_2:55;
then f . (1_ G) in { (f . g) where g is Element of : g in G'' } ;
then reconsider A = { (f . g) where g is Element of : 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 ex g being Element of st
( x = f . g & g in G'' ) ;
hence x in the carrier of H ; :: thesis: verum

end;

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

A1: now

let h1, h2 be Element of ; :: 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 such that
A4: ( h1 = f . a & a in G'' ) by A2;
consider b being Element of such that
A5: ( h2 = f . b & b in G'' ) by A3;
( f . (a * b) = h1 * h2 & a * b in G'' ) by A4, A5, GROUP_2:59, GROUP_6:def 7;
hence h1 * h2 in A ; :: thesis: verum

end;

A6: now

let o be Element of O; :: thesis: for h being Element of st h in A holds
(H ^ o) . h in A
let h be Element of ; :: 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 such that
A7: h = f . g and
A8: g in G'' ;
g in the carrier of G'' by A8, 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 A9: (G ^ o) . g in G'' 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

let h be Element of ; :: thesis: ( h in A implies h " in A )
assume h in A ; :: thesis: h " in A
then consider g being Element of such that
A10: ( h = f . g & g in G'' ) ;
( g " in G'' & h " = f . (g " ) ) by A10, Lm14, GROUP_2:60;
hence h " in A ; :: thesis: verum

end;

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

now

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

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 such that
A12: h = f . g and
A13: g in G'' ;
A14: g in the carrier of G' 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:8;
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 such that
A15: ( [g,h] in R & g in the carrier of G' ) by RELSET_1:52;
( f . g = h & g in G'' ) by A15, FUNCT_1:8, STRUCT_0:def 5;
hence h in A ; :: thesis: verum

end;

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