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 ;

A11: the carrier of H99 = A by A1, A6, Lm14;

take H99 ; :: thesis: the carrier of H99 = f .: the carrier of G9

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

then reconsider A = A as Subset of H by TARSKI:def 3;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;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

A1: now :: thesis: for h1, h2 being Element of H st h1 in A & h2 in A holds

h1 * h2 in A

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;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

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

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;(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

now :: thesis: for h being Element of H st h in A holds

h " in A

then consider H99 being strict StableSubgroup of H such that 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;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

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 ) )

hence
the carrier of H99 = f .: the carrier of G9
by A11, SUBSET_1:3; :: thesis: verum( ( 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 ;

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;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 f .: the carrier of G9
; :: thesis: h in Aassume
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;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

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