let O be set ; :: thesis: for G being GroupWithOperators of O

for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) holds

ex H being strict StableSubgroup of G st the carrier of H = A

let G be GroupWithOperators of O; :: thesis: for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) holds

ex H being strict StableSubgroup of G st the carrier of H = A

let A be Subset of G; :: thesis: ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) implies ex H being strict StableSubgroup of G st the carrier of H = A )

assume A1: A <> {} ; :: thesis: ( ex g1, g2 being Element of G st

( g1 in A & g2 in A & not g1 * g2 in A ) or ex g being Element of G st

( g in A & not g " in A ) or ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

assume A2: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ; :: thesis: ( ex g being Element of G st

( g in A & not g " in A ) or ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

assume for g being Element of G st g in A holds

g " in A ; :: thesis: ( ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

then consider H9 being strict Subgroup of G such that

A3: the carrier of H9 = A by A1, A2, GROUP_2:52;

set m9 = the multF of H9;

set A9 = the carrier of H9;

assume A4: for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = A

for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) holds

ex H being strict StableSubgroup of G st the carrier of H = A

let G be GroupWithOperators of O; :: thesis: for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) holds

ex H being strict StableSubgroup of G st the carrier of H = A

let A be Subset of G; :: thesis: ( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ) & ( for g being Element of G st g in A holds

g " in A ) & ( for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ) implies ex H being strict StableSubgroup of G st the carrier of H = A )

assume A1: A <> {} ; :: thesis: ( ex g1, g2 being Element of G st

( g1 in A & g2 in A & not g1 * g2 in A ) or ex g being Element of G st

( g in A & not g " in A ) or ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

assume A2: for g1, g2 being Element of G st g1 in A & g2 in A holds

g1 * g2 in A ; :: thesis: ( ex g being Element of G st

( g in A & not g " in A ) or ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

assume for g being Element of G st g in A holds

g " in A ; :: thesis: ( ex o being Element of O ex g being Element of G st

( g in A & not (G ^ o) . g in A ) or ex H being strict StableSubgroup of G st the carrier of H = A )

then consider H9 being strict Subgroup of G such that

A3: the carrier of H9 = A by A1, A2, GROUP_2:52;

set m9 = the multF of H9;

set A9 = the carrier of H9;

assume A4: for o being Element of O

for g being Element of G st g in A holds

(G ^ o) . g in A ; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = A

A5: now :: thesis: for H being non empty HGrWOpStr over O

for a9 being Action of O, the carrier of H9 st H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) holds

( H is associative & H is Group-like )

for a9 being Action of O, the carrier of H9 st H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) holds

( H is associative & H is Group-like )

let H be non empty HGrWOpStr over O; :: thesis: for a9 being Action of O, the carrier of H9 st H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) holds

( H is associative & H is Group-like )

let a9 be Action of O, the carrier of H9; :: thesis: ( H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) implies ( H is associative & H is Group-like ) )

assume A6: H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) ; :: thesis: ( H is associative & H is Group-like )

end;( H is associative & H is Group-like )

let a9 be Action of O, the carrier of H9; :: thesis: ( H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) implies ( H is associative & H is Group-like ) )

assume A6: H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) ; :: thesis: ( H is associative & H is Group-like )

now :: thesis: for x, y, z being Element of H holds (x * y) * z = x * (y * z)

hence
H is associative
by GROUP_1:def 3; :: thesis: H is Group-like let x, y, z be Element of H; :: thesis: (x * y) * z = x * (y * z)

reconsider x9 = x, y9 = y, z9 = z as Element of H9 by A6;

(x * y) * z = (x9 * y9) * z9 by A6

.= x9 * (y9 * z9) by GROUP_1:def 3 ;

hence (x * y) * z = x * (y * z) by A6; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of H9 by A6;

(x * y) * z = (x9 * y9) * z9 by A6

.= x9 * (y9 * z9) by GROUP_1:def 3 ;

hence (x * y) * z = x * (y * z) by A6; :: thesis: verum

now :: thesis: ex e being Element of H st

for h being Element of H holds

( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

hence
H is Group-like
by GROUP_1:def 2; :: thesis: verumfor h being Element of H holds

( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

set e9 = 1_ H9;

reconsider e = 1_ H9 as Element of H by A6;

take e = e; :: thesis: for h being Element of H holds

( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

let h be Element of H; :: thesis: ( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

reconsider h9 = h as Element of H9 by A6;

set g9 = h9 " ;

h * e = h9 * (1_ H9) by A6

.= h9 by GROUP_1:def 4 ;

hence h * e = h ; :: thesis: ( e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

e * h = (1_ H9) * h9 by A6

.= h9 by GROUP_1:def 4 ;

hence e * h = h ; :: thesis: ex g being Element of H st

( h * g = e & g * h = e )

reconsider g = h9 " as Element of H by A6;

take g = g; :: thesis: ( h * g = e & g * h = e )

h * g = h9 * (h9 ") by A6

.= 1_ H9 by GROUP_1:def 5 ;

hence h * g = e ; :: thesis: g * h = e

g * h = (h9 ") * h9 by A6

.= 1_ H9 by GROUP_1:def 5 ;

hence g * h = e ; :: thesis: verum

end;reconsider e = 1_ H9 as Element of H by A6;

take e = e; :: thesis: for h being Element of H holds

( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

let h be Element of H; :: thesis: ( h * e = h & e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

reconsider h9 = h as Element of H9 by A6;

set g9 = h9 " ;

h * e = h9 * (1_ H9) by A6

.= h9 by GROUP_1:def 4 ;

hence h * e = h ; :: thesis: ( e * h = h & ex g being Element of H st

( h * g = e & g * h = e ) )

e * h = (1_ H9) * h9 by A6

.= h9 by GROUP_1:def 4 ;

hence e * h = h ; :: thesis: ex g being Element of H st

( h * g = e & g * h = e )

reconsider g = h9 " as Element of H by A6;

take g = g; :: thesis: ( h * g = e & g * h = e )

h * g = h9 * (h9 ") by A6

.= 1_ H9 by GROUP_1:def 5 ;

hence h * g = e ; :: thesis: g * h = e

g * h = (h9 ") * h9 by A6

.= 1_ H9 by GROUP_1:def 5 ;

hence g * h = e ; :: thesis: verum

per cases
( O is empty or not O is empty )
;

end;

suppose A7:
O is empty
; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = A

set a9 = [:{},{(id the carrier of H9)}:];

reconsider a9 = [:{},{(id the carrier of H9)}:] as Action of O, the carrier of H9 by A7, Lm1;

set H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #);

reconsider H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) as non empty HGrWOpStr over O ;

for G9 being Group

for a being Action of O, the carrier of G9 st a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) holds

a is distributive by A7;

then reconsider H = H as GroupWithOperators of O by A5, Def5;

A8: the carrier of H c= the carrier of G by GROUP_2:def 5;

then H is Subgroup of G by A8, GROUP_2:def 5;

then reconsider H = H as strict StableSubgroup of G by A9, Def7;

take H ; :: thesis: the carrier of H = A

thus the carrier of H = A by A3; :: thesis: verum

end;reconsider a9 = [:{},{(id the carrier of H9)}:] as Action of O, the carrier of H9 by A7, Lm1;

set H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #);

reconsider H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) as non empty HGrWOpStr over O ;

for G9 being Group

for a being Action of O, the carrier of G9 st a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) holds

a is distributive by A7;

then reconsider H = H as GroupWithOperators of O by A5, Def5;

A8: the carrier of H c= the carrier of G by GROUP_2:def 5;

A9: now :: thesis: for o being Element of O holds H ^ o = (G ^ o) | the carrier of H

the multF of H = the multF of G || the carrier of H
by GROUP_2:def 5;let o be Element of O; :: thesis: H ^ o = (G ^ o) | the carrier of H

.= (id the carrier of G) | the carrier of H by A13, A10 ;

hence H ^ o = (G ^ o) | the carrier of H by A7, Def6; :: thesis: verum

end;A10: now :: thesis: for x, y being object st [x,y] in (id the carrier of G) | the carrier of H holds

[x,y] in id the carrier of H

[x,y] in id the carrier of H

let x, y be object ; :: thesis: ( [x,y] in (id the carrier of G) | the carrier of H implies [x,y] in id the carrier of H )

assume A11: [x,y] in (id the carrier of G) | the carrier of H ; :: thesis: [x,y] in id the carrier of H

then [x,y] in id the carrier of G by RELAT_1:def 11;

then A12: x = y by RELAT_1:def 10;

x in the carrier of H by A11, RELAT_1:def 11;

hence [x,y] in id the carrier of H by A12, RELAT_1:def 10; :: thesis: verum

end;assume A11: [x,y] in (id the carrier of G) | the carrier of H ; :: thesis: [x,y] in id the carrier of H

then [x,y] in id the carrier of G by RELAT_1:def 11;

then A12: x = y by RELAT_1:def 10;

x in the carrier of H by A11, RELAT_1:def 11;

hence [x,y] in id the carrier of H by A12, RELAT_1:def 10; :: thesis: verum

A13: now :: thesis: for x, y being object st [x,y] in id the carrier of H holds

[x,y] in (id the carrier of G) | the carrier of H

H ^ o =
id the carrier of H
by A7, Def6
[x,y] in (id the carrier of G) | the carrier of H

let x, y be object ; :: thesis: ( [x,y] in id the carrier of H implies [x,y] in (id the carrier of G) | the carrier of H )

assume A14: [x,y] in id the carrier of H ; :: thesis: [x,y] in (id the carrier of G) | the carrier of H

then A15: x in the carrier of H by RELAT_1:def 10;

x = y by A14, RELAT_1:def 10;

then [x,y] in id the carrier of G by A8, A15, RELAT_1:def 10;

hence [x,y] in (id the carrier of G) | the carrier of H by A15, RELAT_1:def 11; :: thesis: verum

end;assume A14: [x,y] in id the carrier of H ; :: thesis: [x,y] in (id the carrier of G) | the carrier of H

then A15: x in the carrier of H by RELAT_1:def 10;

x = y by A14, RELAT_1:def 10;

then [x,y] in id the carrier of G by A8, A15, RELAT_1:def 10;

hence [x,y] in (id the carrier of G) | the carrier of H by A15, RELAT_1:def 11; :: thesis: verum

.= (id the carrier of G) | the carrier of H by A13, A10 ;

hence H ^ o = (G ^ o) | the carrier of H by A7, Def6; :: thesis: verum

then H is Subgroup of G by A8, GROUP_2:def 5;

then reconsider H = H as strict StableSubgroup of G by A9, Def7;

take H ; :: thesis: the carrier of H = A

thus the carrier of H = A by A3; :: thesis: verum

suppose A16:
not O is empty
; :: thesis: ex H being strict StableSubgroup of G st the carrier of H = A

set a9 = { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } ;

then reconsider a9 = a9 as Action of O, the carrier of H9 by A20, FUNCT_2:2;

reconsider H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) as non empty HGrWOpStr over O ;

A31: the multF of H = the multF of G || the carrier of H by GROUP_2:def 5;

( H is Group-like & the carrier of H c= the carrier of G ) by A5, GROUP_2:def 5;

then A32: H is Subgroup of G by A31, GROUP_2:def 5;

take H ; :: thesis: the carrier of H = A

thus the carrier of H = A by A3; :: thesis: verum

end;now :: thesis: for x being object st x in { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } holds

ex y1, y2 being object st x = [y1,y2]

then reconsider a9 = { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } as Relation by RELAT_1:def 1;ex y1, y2 being object st x = [y1,y2]

let x be object ; :: thesis: ( x in { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } implies ex y1, y2 being object st x = [y1,y2] )

assume x in { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } ; :: thesis: ex y1, y2 being object st x = [y1,y2]

then ex o being Element of O st x = [o,((G ^ o) | the carrier of H9)] ;

hence ex y1, y2 being object st x = [y1,y2] ; :: thesis: verum

end;assume x in { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } ; :: thesis: ex y1, y2 being object st x = [y1,y2]

then ex o being Element of O st x = [o,((G ^ o) | the carrier of H9)] ;

hence ex y1, y2 being object st x = [y1,y2] ; :: thesis: verum

A17: now :: thesis: for x being object st x in O holds

ex y being object st [x,y] in a9

ex y being object st [x,y] in a9

let x be object ; :: thesis: ( x in O implies ex y being object st [x,y] in a9 )

assume x in O ; :: thesis: ex y being object st [x,y] in a9

then reconsider o = x as Element of O ;

reconsider y = (G ^ o) | the carrier of H9 as object ;

take y = y; :: thesis: [x,y] in a9

thus [x,y] in a9 ; :: thesis: verum

end;assume x in O ; :: thesis: ex y being object st [x,y] in a9

then reconsider o = x as Element of O ;

reconsider y = (G ^ o) | the carrier of H9 as object ;

take y = y; :: thesis: [x,y] in a9

thus [x,y] in a9 ; :: thesis: verum

now :: thesis: for x being object st ex y being object st [x,y] in a9 holds

x in O

then A20:
dom a9 = O
by A17, XTUPLE_0:def 12;x in O

let x be object ; :: thesis: ( ex y being object st [x,y] in a9 implies x in O )

given y being object such that A18: [x,y] in a9 ; :: thesis: x in O

consider o being Element of O such that

A19: [x,y] = [o,((G ^ o) | the carrier of H9)] by A18;

o in O by A16;

hence x in O by A19, XTUPLE_0:1; :: thesis: verum

end;given y being object such that A18: [x,y] in a9 ; :: thesis: x in O

consider o being Element of O such that

A19: [x,y] = [o,((G ^ o) | the carrier of H9)] by A18;

o in O by A16;

hence x in O by A19, XTUPLE_0:1; :: thesis: verum

now :: thesis: for x, y1, y2 being object st [x,y1] in a9 & [x,y2] in a9 holds

y1 = y2

then reconsider a9 = a9 as Function by FUNCT_1:def 1;y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in a9 & [x,y2] in a9 implies y1 = y2 )

assume [x,y1] in a9 ; :: thesis: ( [x,y2] in a9 implies y1 = y2 )

then consider o1 being Element of O such that

A21: [x,y1] = [o1,((G ^ o1) | the carrier of H9)] ;

A22: x = o1 by A21, XTUPLE_0:1;

assume [x,y2] in a9 ; :: thesis: y1 = y2

then consider o2 being Element of O such that

A23: [x,y2] = [o2,((G ^ o2) | the carrier of H9)] ;

x = o2 by A23, XTUPLE_0:1;

hence y1 = y2 by A21, A23, A22, XTUPLE_0:1; :: thesis: verum

end;assume [x,y1] in a9 ; :: thesis: ( [x,y2] in a9 implies y1 = y2 )

then consider o1 being Element of O such that

A21: [x,y1] = [o1,((G ^ o1) | the carrier of H9)] ;

A22: x = o1 by A21, XTUPLE_0:1;

assume [x,y2] in a9 ; :: thesis: y1 = y2

then consider o2 being Element of O such that

A23: [x,y2] = [o2,((G ^ o2) | the carrier of H9)] ;

x = o2 by A23, XTUPLE_0:1;

hence y1 = y2 by A21, A23, A22, XTUPLE_0:1; :: thesis: verum

now :: thesis: for y being object st y in rng a9 holds

y in Funcs ( the carrier of H9, the carrier of H9)

then
rng a9 c= Funcs ( the carrier of H9, the carrier of H9)
;y in Funcs ( the carrier of H9, the carrier of H9)

let y be object ; :: thesis: ( y in rng a9 implies y in Funcs ( the carrier of H9, the carrier of H9) )

assume y in rng a9 ; :: thesis: y in Funcs ( the carrier of H9, the carrier of H9)

then consider x being object such that

A24: ( x in dom a9 & y = a9 . x ) by FUNCT_1:def 3;

[x,y] in a9 by A24, FUNCT_1:1;

then consider o being Element of O such that

A25: [x,y] = [o,((G ^ o) | the carrier of H9)] ;

end;assume y in rng a9 ; :: thesis: y in Funcs ( the carrier of H9, the carrier of H9)

then consider x being object such that

A24: ( x in dom a9 & y = a9 . x ) by FUNCT_1:def 3;

[x,y] in a9 by A24, FUNCT_1:1;

then consider o being Element of O such that

A25: [x,y] = [o,((G ^ o) | the carrier of H9)] ;

now :: thesis: ex f being Function st

( y = f & dom f = the carrier of H9 & rng f c= the carrier of H9 )

hence
y in Funcs ( the carrier of H9, the carrier of H9)
by FUNCT_2:def 2; :: thesis: verum( y = f & dom f = the carrier of H9 & rng f c= the carrier of H9 )

reconsider f = (G ^ o) | the carrier of H9 as Function ;

take f = f; :: thesis: ( y = f & dom f = the carrier of H9 & rng f c= the carrier of H9 )

A26: dom ((G ^ o) | the carrier of H9) = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:65

.= (dom (G ^ o)) /\ the carrier of H9 by FUNCT_1:19

.= the carrier of G /\ the carrier of H9 by FUNCT_2:def 1 ;

thus y = f by A25, XTUPLE_0:1; :: thesis: ( dom f = the carrier of H9 & rng f c= the carrier of H9 )

the carrier of H9 c= the carrier of G by GROUP_2:def 5;

hence A27: dom f = the carrier of H9 by A26, XBOOLE_1:28; :: thesis: rng f c= the carrier of H9

end;take f = f; :: thesis: ( y = f & dom f = the carrier of H9 & rng f c= the carrier of H9 )

A26: dom ((G ^ o) | the carrier of H9) = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:65

.= (dom (G ^ o)) /\ the carrier of H9 by FUNCT_1:19

.= the carrier of G /\ the carrier of H9 by FUNCT_2:def 1 ;

thus y = f by A25, XTUPLE_0:1; :: thesis: ( dom f = the carrier of H9 & rng f c= the carrier of H9 )

the carrier of H9 c= the carrier of G by GROUP_2:def 5;

hence A27: dom f = the carrier of H9 by A26, XBOOLE_1:28; :: thesis: rng f c= the carrier of H9

now :: thesis: for y being object st y in rng f holds

y in the carrier of H9

hence
rng f c= the carrier of H9
; :: thesis: verumy in the carrier of H9

let y be object ; :: thesis: ( y in rng f implies y in the carrier of H9 )

A28: dom f = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:65;

assume y in rng f ; :: thesis: y in the carrier of H9

then consider x being object such that

A29: x in dom f and

A30: y = f . x by FUNCT_1:def 3;

y = ((G ^ o) * (id the carrier of H9)) . x by A30, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . x) by A28, A29, FUNCT_1:12

.= (G ^ o) . x by A27, A29, FUNCT_1:18 ;

hence y in the carrier of H9 by A4, A3, A27, A29; :: thesis: verum

end;A28: dom f = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:65;

assume y in rng f ; :: thesis: y in the carrier of H9

then consider x being object such that

A29: x in dom f and

A30: y = f . x by FUNCT_1:def 3;

y = ((G ^ o) * (id the carrier of H9)) . x by A30, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . x) by A28, A29, FUNCT_1:12

.= (G ^ o) . x by A27, A29, FUNCT_1:18 ;

hence y in the carrier of H9 by A4, A3, A27, A29; :: thesis: verum

then reconsider a9 = a9 as Action of O, the carrier of H9 by A20, FUNCT_2:2;

reconsider H = HGrWOpStr(# the carrier of H9, the multF of H9,a9 #) as non empty HGrWOpStr over O ;

A31: the multF of H = the multF of G || the carrier of H by GROUP_2:def 5;

( H is Group-like & the carrier of H c= the carrier of G ) by A5, GROUP_2:def 5;

then A32: H is Subgroup of G by A31, GROUP_2:def 5;

now :: thesis: for G9 being Group

for a being Action of O, the carrier of G9 st a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) holds

a is distributive

then reconsider H = H as GroupWithOperators of O by A5, Def5;for a being Action of O, the carrier of G9 st a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) holds

a is distributive

let G9 be Group; :: thesis: for a being Action of O, the carrier of G9 st a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) holds

a is distributive

let a be Action of O, the carrier of G9; :: thesis: ( a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) implies a is distributive )

assume A33: a = the action of H ; :: thesis: ( multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) implies a is distributive )

assume A34: multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) ; :: thesis: a is distributive

end;a is distributive

let a be Action of O, the carrier of G9; :: thesis: ( a = the action of H & multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) implies a is distributive )

assume A33: a = the action of H ; :: thesis: ( multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) implies a is distributive )

assume A34: multMagma(# the carrier of G9, the multF of G9 #) = multMagma(# the carrier of H, the multF of H #) ; :: thesis: a is distributive

now :: thesis: for o being Element of O st o in O holds

a . o is Homomorphism of G9,G9

hence
a is distributive
; :: thesis: veruma . o is Homomorphism of G9,G9

let o be Element of O; :: thesis: ( o in O implies a . o is Homomorphism of G9,G9 )

assume o in O ; :: thesis: a . o is Homomorphism of G9,G9

then A35: o in dom a by FUNCT_2:def 1;

then a . o in rng a by FUNCT_1:3;

then consider f being Function such that

A36: a . o = f and

A37: ( dom f = the carrier of G9 & rng f c= the carrier of G9 ) by FUNCT_2:def 2;

reconsider f = f as Function of G9,G9 by A37, FUNCT_2:2;

[o,(a . o)] in a9 by A33, A35, FUNCT_1:1;

then consider o9 being Element of O such that

A38: [o,(a . o)] = [o9,((G ^ o9) | the carrier of H9)] ;

A39: ( o = o9 & a . o = (G ^ o9) | the carrier of H9 ) by A38, XTUPLE_0:1;

end;assume o in O ; :: thesis: a . o is Homomorphism of G9,G9

then A35: o in dom a by FUNCT_2:def 1;

then a . o in rng a by FUNCT_1:3;

then consider f being Function such that

A36: a . o = f and

A37: ( dom f = the carrier of G9 & rng f c= the carrier of G9 ) by FUNCT_2:def 2;

reconsider f = f as Function of G9,G9 by A37, FUNCT_2:2;

[o,(a . o)] in a9 by A33, A35, FUNCT_1:1;

then consider o9 being Element of O such that

A38: [o,(a . o)] = [o9,((G ^ o9) | the carrier of H9)] ;

A39: ( o = o9 & a . o = (G ^ o9) | the carrier of H9 ) by A38, XTUPLE_0:1;

now :: thesis: for a9, b9 being Element of G9 holds f . (a9 * b9) = (f . a9) * (f . b9)

hence
a . o is Homomorphism of G9,G9
by A36, GROUP_6:def 6; :: thesis: verumlet a9, b9 be Element of G9; :: thesis: f . (a9 * b9) = (f . a9) * (f . b9)

b9 in the carrier of H9 by A34;

then A40: b9 in dom (id the carrier of H9) ;

reconsider a = a9, b = b9 as Element of H by A34;

reconsider g1 = a, g2 = b as Element of G by GROUP_2:42;

a9 in the carrier of H9 by A34;

then A41: a9 in dom (id the carrier of H9) ;

reconsider h1 = (G ^ o) . g1, h2 = (G ^ o) . g2 as Element of H by A4, A3;

a9 * b9 in the carrier of H9 by A34;

then A42: a9 * b9 in dom (id the carrier of H9) ;

A43: f . b9 = ((G ^ o) * (id the carrier of H9)) . b9 by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . b9) by A40, FUNCT_1:13

.= h2 ;

A44: f . a9 = ((G ^ o) * (id the carrier of H9)) . a9 by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . a9) by A41, FUNCT_1:13

.= h1 ;

thus f . (a9 * b9) = ((G ^ o) * (id the carrier of H9)) . (a9 * b9) by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . (a9 * b9)) by A42, FUNCT_1:13

.= (G ^ o) . (a * b) by A34

.= (G ^ o) . (g1 * g2) by A32, GROUP_2:43

.= ((G ^ o) . g1) * ((G ^ o) . g2) by GROUP_6:def 6

.= h1 * h2 by A32, GROUP_2:43

.= (f . a9) * (f . b9) by A34, A44, A43 ; :: thesis: verum

end;b9 in the carrier of H9 by A34;

then A40: b9 in dom (id the carrier of H9) ;

reconsider a = a9, b = b9 as Element of H by A34;

reconsider g1 = a, g2 = b as Element of G by GROUP_2:42;

a9 in the carrier of H9 by A34;

then A41: a9 in dom (id the carrier of H9) ;

reconsider h1 = (G ^ o) . g1, h2 = (G ^ o) . g2 as Element of H by A4, A3;

a9 * b9 in the carrier of H9 by A34;

then A42: a9 * b9 in dom (id the carrier of H9) ;

A43: f . b9 = ((G ^ o) * (id the carrier of H9)) . b9 by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . b9) by A40, FUNCT_1:13

.= h2 ;

A44: f . a9 = ((G ^ o) * (id the carrier of H9)) . a9 by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . a9) by A41, FUNCT_1:13

.= h1 ;

thus f . (a9 * b9) = ((G ^ o) * (id the carrier of H9)) . (a9 * b9) by A36, A39, RELAT_1:65

.= (G ^ o) . ((id the carrier of H9) . (a9 * b9)) by A42, FUNCT_1:13

.= (G ^ o) . (a * b) by A34

.= (G ^ o) . (g1 * g2) by A32, GROUP_2:43

.= ((G ^ o) . g1) * ((G ^ o) . g2) by GROUP_6:def 6

.= h1 * h2 by A32, GROUP_2:43

.= (f . a9) * (f . b9) by A34, A44, A43 ; :: thesis: verum

now :: thesis: for o being Element of O holds H ^ o = (G ^ o) | the carrier of H

then reconsider H = H as strict StableSubgroup of G by A32, Def7;let o be Element of O; :: thesis: H ^ o = (G ^ o) | the carrier of H

o in O by A16;

then o in dom a9 by FUNCT_2:def 1;

then [o,(a9 . o)] in a9 by FUNCT_1:1;

then consider o9 being Element of O such that

A45: [o,(a9 . o)] = [o9,((G ^ o9) | the carrier of H9)] ;

( o = o9 & a9 . o = (G ^ o9) | the carrier of H9 ) by A45, XTUPLE_0:1;

hence H ^ o = (G ^ o) | the carrier of H by A16, Def6; :: thesis: verum

end;o in O by A16;

then o in dom a9 by FUNCT_2:def 1;

then [o,(a9 . o)] in a9 by FUNCT_1:1;

then consider o9 being Element of O such that

A45: [o,(a9 . o)] = [o9,((G ^ o9) | the carrier of H9)] ;

( o = o9 & a9 . o = (G ^ o9) | the carrier of H9 ) by A45, XTUPLE_0:1;

hence H ^ o = (G ^ o) | the carrier of H by A16, Def6; :: thesis: verum

take H ; :: thesis: the carrier of H = A

thus the carrier of H = A by A3; :: thesis: verum