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 ;
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 )
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 )
now :: thesis: for x, y, z being Element of H holds (x * y) * z = x * (y * z)
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;
hence H is associative by GROUP_1:def 3; :: thesis: H is Group-like
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 ) )
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;
hence H is Group-like by GROUP_1:def 2; :: thesis: verum
end;
per cases ( O is empty or not O is empty ) ;
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 ;
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 ;
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
let o be Element of O; :: thesis: H ^ o = (G ^ o) | the carrier of H
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
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 ;
hence [x,y] in id the carrier of H by ; :: thesis: verum
end;
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
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 ;
then [x,y] in id the carrier of G by ;
hence [x,y] in (id the carrier of G) | the carrier of H by ; :: thesis: verum
end;
H ^ o = id the carrier of H by
.= (id the carrier of G) | the carrier of H by ;
hence H ^ o = (G ^ o) | the carrier of H by ; :: thesis: verum
end;
the multF of H = the multF of G || the carrier of H by GROUP_2:def 5;
then H is Subgroup of G by ;
then reconsider H = H as strict StableSubgroup of G by ;
take H ; :: thesis: the carrier of H = A
thus the carrier of H = A by A3; :: thesis: verum
end;
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 } ;
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]
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;
then reconsider a9 = { [o,((G ^ o) | the carrier of H9)] where o is Element of O : verum } as Relation by RELAT_1:def 1;
A17: now :: thesis: for x being object st x in O holds
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;
now :: thesis: for x being object st ex y being object st [x,y] in a9 holds
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 ; :: thesis: verum
end;
then A20: dom a9 = O by ;
now :: thesis: for x, y1, y2 being object st [x,y1] in a9 & [x,y2] in a9 holds
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 ;
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 ;
hence y1 = y2 by ; :: thesis: verum
end;
then reconsider a9 = a9 as Function by FUNCT_1:def 1;
now :: thesis: for y being object st y in rng a9 holds
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 ;
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 )
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 ; :: 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 ; :: 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
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
.= (G ^ o) . ((id the carrier of H9) . x) by
.= (G ^ o) . x by ;
hence y in the carrier of H9 by A4, A3, A27, A29; :: thesis: verum
end;
hence rng f c= the carrier of H9 ; :: thesis: verum
end;
hence y in Funcs ( the carrier of H9, the carrier of H9) by FUNCT_2:def 2; :: thesis: verum
end;
then rng a9 c= Funcs ( the carrier of H9, the carrier of H9) ;
then reconsider a9 = a9 as Action of O, the carrier of H9 by ;
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 ;
then A32: H is Subgroup of G by ;
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
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
now :: thesis: for o being Element of O st o in O holds
a . 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 ;
[o,(a . o)] in a9 by ;
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 ;
now :: thesis: for a9, b9 being Element of G9 holds f . (a9 * b9) = (f . a9) * (f . b9)
let 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
.= (G ^ o) . ((id the carrier of H9) . b9) by
.= h2 ;
A44: f . a9 = ((G ^ o) * (id the carrier of H9)) . a9 by
.= (G ^ o) . ((id the carrier of H9) . a9) by
.= h1 ;
thus f . (a9 * b9) = ((G ^ o) * (id the carrier of H9)) . (a9 * b9) by
.= (G ^ o) . ((id the carrier of H9) . (a9 * b9)) by
.= (G ^ o) . (a * b) by A34
.= (G ^ o) . (g1 * g2) by
.= ((G ^ o) . g1) * ((G ^ o) . g2) by GROUP_6:def 6
.= h1 * h2 by
.= (f . a9) * (f . b9) by ; :: thesis: verum
end;
hence a . o is Homomorphism of G9,G9 by ; :: thesis: verum
end;
hence a is distributive ; :: thesis: verum
end;
then reconsider H = H as GroupWithOperators of O by ;
now :: thesis: for o being Element of O holds H ^ o = (G ^ o) | the carrier of H
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 ;
hence H ^ o = (G ^ o) | the carrier of H by ; :: thesis: verum
end;
then reconsider H = H as strict StableSubgroup of G by ;
take H ; :: thesis: the carrier of H = A
thus the carrier of H = A by A3; :: thesis: verum
end;
end;