let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let A be Subset of G; :: thesis:
assume A1: A <> {} ; :: thesis:
assume A2: for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ; :: thesis:
assume for g being Element of G st g in A holds
g " in A ; :: thesis:
then consider H9 being strict Subgroup of G such that
A3: the carrier of H9 = A by A1, A2, GROUP_2:61;
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:

A5: now

let H be non empty HGrWOpStr of O; :: thesis:
let a9 be Action of O,the carrier of H9; :: thesis:
assume A6: H = HGrWOpStr(# the carrier of H9,the multF of H9,a9 #) ; :: thesis:

let x, y, z be Element of H; :: thesis:
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 4 ;
hence (x * y) * z = x * (y * z) by A6; :: thesis:

end;

hence H is associative by GROUP_1:def 4; :: thesis:

now

set e9 = 1_ H9;
reconsider e = 1_ H9 as Element of H by A6;
take e = e; :: thesis:
let h be Element of H; :: thesis:
reconsider h9 = h as Element of H9 by A6;
set g9 = h9 " ;
h * e = h9 * (1_ H9) by A6
.= h9 by GROUP_1:def 5 ;
hence h * e = h ; :: thesis:
e * h = (1_ H9) * h9 by A6
.= h9 by GROUP_1:def 5 ;
hence e * h = h ; :: thesis:
reconsider g = h9 " as Element of H by A6;
take g = g; :: thesis:
h * g = h9 * (h9 " ) by A6
.= 1_ H9 by GROUP_1:def 6 ;
hence h * g = e ; :: thesis:
g * h = (h9 " ) * h9 by A6
.= 1_ H9 by GROUP_1:def 6 ;
hence g * h = e ; :: thesis:

end;

hence H is Group-like by GROUP_1:def 3; :: thesis:

end;

per cases ;

suppose A7: O is empty ; :: thesis:

set a9 = [:{} ,{(id the carrier of H9)}:];
reconsider a9 = [:{} ,{(id the carrier of H9)}:] as Action of O,the carrier of H9 by A7, Lm2;
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 of O ;

now

let G9 be Group; :: thesis:
let a be Action of O,the carrier of G9; :: thesis:
assume a = the action of H ; :: thesis:
assume multMagma(# the carrier of G9,the multF of G9 #) = multMagma(# the carrier of H,the multF of H #) ; :: thesis:
for o being Element of O st o in O holds
a . o is Homomorphism of G9,G9 by A7;
hence a is distributive by Def4; :: thesis:

end;

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

let o be Element of O; :: thesis:

A10: now

let x, y be set ; :: thesis:
assume A11: [x,y] in (id the carrier of G) | the carrier of H ; :: thesis:
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:

end;

A13: now

let x, y be set ; :: thesis:
assume A14: [x,y] in id the carrier of H ; :: thesis:
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:

end;

H ^ o = id the carrier of H by A7, Def6
.= (id the carrier of G) | the carrier of H by A13, A10, RELAT_1:def 2 ;
hence H ^ o = (G ^ o) | the carrier of H by A7, Def6; :: thesis:

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 A8, GROUP_2:def 5;
then reconsider H = H as strict StableSubgroup of G by A9, Def7;
take H ; :: thesis:
thus the carrier of H = A by A3; :: thesis:

end;

suppose A16: not O is empty ; :: thesis:

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

now

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

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

let x be set ; :: thesis:
assume x in O ; :: thesis:
then reconsider o = x as Element of O ;
reconsider y = (G ^ o) | the carrier of H9 as set ;
take y = y; :: thesis:
thus [x,y] in a9 ; :: thesis:

end;

now

let x be set ; :: thesis:
given y being set such that A18: [x,y] in a9 ; :: thesis:
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, ZFMISC_1:33; :: thesis:

end;

then A20: dom a9 = O by A17, RELAT_1:def 4;

now

let x, y1, y2 be set ; :: thesis:
assume [x,y1] in a9 ; :: thesis:
then consider o1 being Element of O such that
A21: [x,y1] = [o1,((G ^ o1) | the carrier of H9)] ;
A22: x = o1 by A21, ZFMISC_1:33;
assume [x,y2] in a9 ; :: thesis:
then consider o2 being Element of O such that
A23: [x,y2] = [o2,((G ^ o2) | the carrier of H9)] ;
x = o2 by A23, ZFMISC_1:33;
hence y1 = y2 by A21, A23, A22, ZFMISC_1:33; :: thesis:

end;

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

now

let y be set ; :: thesis:
assume y in rng a9 ; :: thesis:
then consider x being set such that
A24: ( x in dom a9 & y = a9 . x ) by FUNCT_1:def 5;
[x,y] in a9 by A24, FUNCT_1:8;
then consider o being Element of O such that
A25: [x,y] = [o,((G ^ o) | the carrier of H9)] ;

now

reconsider f = (G ^ o) | the carrier of H9 as Function ;
take f = f; :: thesis:
A26: dom ((G ^ o) | the carrier of H9) = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:94
.= (dom (G ^ o)) /\ the carrier of H9 by FUNCT_1:37
.= the carrier of G /\ the carrier of H9 by FUNCT_2:def 1 ;
thus y = f by A25, ZFMISC_1:33; :: thesis:
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:

now

let y be set ; :: thesis:
A28: dom f = dom ((G ^ o) * (id the carrier of H9)) by RELAT_1:94;
assume y in rng f ; :: thesis:
then consider x being set such that
A29: x in dom f and
A30: y = f . x by FUNCT_1:def 5;
y = ((G ^ o) * (id the carrier of H9)) . x by A30, RELAT_1:94
.= (G ^ o) . ((id the carrier of H9) . x) by A28, A29, FUNCT_1:22
.= (G ^ o) . x by A27, A29, FUNCT_1:35 ;
hence y in the carrier of H9 by A4, A3, A27, A29; :: thesis:

end;

hence rng f c= the carrier of H9 by TARSKI:def 3; :: thesis:

end;

hence y in Funcs the carrier of H9,the carrier of H9 by FUNCT_2:def 2; :: thesis:

end;

then rng a9 c= Funcs the carrier of H9,the carrier of H9 by TARSKI:def 3;
then reconsider a9 = a9 as Action of O,the carrier of H9 by A20, FUNCT_2:4;
reconsider H = HGrWOpStr(# the carrier of H9,the multF of H9,a9 #) as non empty HGrWOpStr of 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

let G9 be Group; :: thesis:
let a be Action of O,the carrier of G9; :: thesis:
assume A33: a = the action of H ; :: thesis:
assume A34: multMagma(# the carrier of G9,the multF of G9 #) = multMagma(# the carrier of H,the multF of H #) ; :: thesis:

now

let o be Element of O; :: thesis:
assume o in O ; :: thesis:
then A35: o in dom a by FUNCT_2:def 1;
then a . o in rng a by FUNCT_1:12;
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:4;
[o,(a . o)] in a9 by A33, A35, FUNCT_1:8;
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, ZFMISC_1:33;

now

let a9, b9 be Element of G9; :: thesis:
b9 in the carrier of H9 by A34;
then A40: b9 in dom (id the carrier of H9) by RELAT_1:71;
reconsider a = a9, b = b9 as Element of H by A34;
reconsider g1 = a, g2 = b as Element of G by GROUP_2:51;
a9 in the carrier of H9 by A34;
then A41: a9 in dom (id the carrier of H9) by RELAT_1:71;
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) by RELAT_1:71;
A43: f . b9 = ((G ^ o) * (id the carrier of H9)) . b9 by A36, A39, RELAT_1:94
.= (G ^ o) . ((id the carrier of H9) . b9) by A40, FUNCT_1:23
.= h2 by FUNCT_1:35 ;
A44: f . a9 = ((G ^ o) * (id the carrier of H9)) . a9 by A36, A39, RELAT_1:94
.= (G ^ o) . ((id the carrier of H9) . a9) by A41, FUNCT_1:23
.= h1 by FUNCT_1:35 ;
thus f . (a9 * b9) = ((G ^ o) * (id the carrier of H9)) . (a9 * b9) by A36, A39, RELAT_1:94
.= (G ^ o) . ((id the carrier of H9) . (a9 * b9)) by A42, FUNCT_1:23
.= (G ^ o) . (a * b) by A34, FUNCT_1:35
.= (G ^ o) . (g1 * g2) by A32, GROUP_2:52
.= ((G ^ o) . g1) * ((G ^ o) . g2) by GROUP_6:def 7
.= h1 * h2 by A32, GROUP_2:52
.= (f . a9) * (f . b9) by A34, A44, A43 ; :: thesis:

end;

hence a . o is Homomorphism of G9,G9 by A36, GROUP_6:def 7; :: thesis:

end;

hence a is distributive by Def4; :: thesis:

end;

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

now

let o be Element of O; :: thesis:
o in O by A16;
then o in dom a9 by FUNCT_2:def 1;
then [o,(a9 . o)] in a9 by FUNCT_1:8;
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, ZFMISC_1:33;
hence H ^ o = (G ^ o) | the carrier of H by A16, Def6; :: thesis:

end;

then reconsider H = H as strict StableSubgroup of G by A32, Def7;
take H ; :: thesis:
thus the carrier of H = A by A3; :: thesis:

end;