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 A3: for g being Element of G st g in A holds
g " in A ; :: thesis:
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:
consider H' being strict Subgroup of G such that
A5: the carrier of H' = A by A1, A2, A3, GROUP_2:61;
set A' = the carrier of H';
set m' = the multF of H';

A6: now

let H be non empty HGrWOpStr of O; :: thesis:
let a' be Action of O,the carrier of H'; :: thesis:
assume A7: H = HGrWOpStr(# the carrier of H',the multF of H',a' #) ; :: thesis:

now

let x, y, z be Element of H; :: thesis:
reconsider x' = x, y' = y, z' = z as Element of H' by A7;
(x * y) * z = (x' * y') * z' by A7
.= x' * (y' * z') by GROUP_1:def 4 ;
hence (x * y) * z = x * (y * z) by A7; :: thesis:

end;

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

now

set e' = 1_ H';
reconsider e = 1_ H' as Element of H by A7;
take e = e; :: thesis:
let h be Element of H; :: thesis:
reconsider h' = h as Element of H' by A7;
h * e = h' * (1_ H') by A7
.= h' by GROUP_1:def 5 ;
hence h * e = h ; :: thesis:
e * h = (1_ H') * h' by A7
.= h' by GROUP_1:def 5 ;
hence e * h = h ; :: thesis:
set g' = h' " ;
reconsider g = h' " as Element of H by A7;
take g = g; :: thesis:
h * g = h' * (h' " ) by A7
.= 1_ H' by GROUP_1:def 6 ;
hence h * g = e ; :: thesis:
g * h = (h' " ) * h' by A7
.= 1_ H' 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 A8: O is empty ; :: thesis:

set a' = [:{} ,{(id the carrier of H')}:];
reconsider a' = [:{} ,{(id the carrier of H')}:] as Action of O,the carrier of H' by A8, Lm2;
set H = HGrWOpStr(# the carrier of H',the multF of H',a' #);
reconsider H = HGrWOpStr(# the carrier of H',the multF of H',a' #) as non empty HGrWOpStr of O ;

now

let G' be Group; :: thesis:
let a be Action of O,the carrier of G'; :: thesis:
assume a = the action of H ; :: thesis:
assume multMagma(# the carrier of G',the multF of G' #) = 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 G',G' by A8;
hence a is distributive by Def4; :: thesis:

end;

then reconsider H = H as GroupWithOperators of O by A6, Def5;
A9: ( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;
then A10: H is Subgroup of G by GROUP_2:def 5;

now

let o be Element of O; :: thesis:

A11: now

let x, y be set ; :: thesis:
assume [x,y] in id the carrier of H ; :: thesis:
then A12: ( x in the carrier of H & x = y ) by RELAT_1:def 10;
then [x,y] in id the carrier of G by A9, RELAT_1:def 10;
hence [x,y] in (id the carrier of G) | the carrier of H by A12, RELAT_1:def 11; :: thesis:

end;

A13: now

let x, y be set ; :: thesis:
assume [x,y] in (id the carrier of G) | the carrier of H ; :: thesis:
then A14: ( x in the carrier of H & [x,y] in id the carrier of G ) by RELAT_1:def 11;
then ( x in the carrier of G & x = y ) by RELAT_1:def 10;
hence [x,y] in id the carrier of H by A14, RELAT_1:def 10; :: thesis:

end;

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

end;

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

end;

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

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

now

let x be set ; :: thesis:
assume x in { [o,((G ^ o) | the carrier of H')] where o is Element of O : verum } ; :: thesis:
then consider o being Element of O such that
A16: x = [o,((G ^ o) | the carrier of H')] ;
thus ex y1, y2 being set st x = [y1,y2] by A16; :: thesis:

end;

then reconsider a' = { [o,((G ^ o) | the carrier of H')] where o is Element of O : verum } as Relation by RELAT_1:def 1;

A17: now

A18: 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 H' as set ;
take y = y; :: thesis:
thus [x,y] in a' ; :: thesis:

end;

now

let x be set ; :: thesis:
given y being set such that A19: [x,y] in a' ; :: thesis:
consider o being Element of O such that
A20: [x,y] = [o,((G ^ o) | the carrier of H')] by A19;
o in O by A15;
hence x in O by A20, ZFMISC_1:33; :: thesis:

end;

hence dom a' = O by A18, RELAT_1:def 4; :: thesis:

end;

now

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

end;

then reconsider a' = a' as Function by FUNCT_1:def 1;

now

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

now

reconsider f = (G ^ o) | the carrier of H' as Function ;
take f = f; :: thesis:
thus y = f by A24, ZFMISC_1:33; :: thesis:
A25: the carrier of H' c= the carrier of G by GROUP_2:def 5;
dom ((G ^ o) | the carrier of H') = dom ((G ^ o) * (id the carrier of H')) by RELAT_1:94
.= (dom (G ^ o)) /\ the carrier of H' by FUNCT_1:37
.= the carrier of G /\ the carrier of H' by FUNCT_2:def 1 ;
hence A27: dom f = the carrier of H' by A25, XBOOLE_1:28; :: thesis:

now

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

end;

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

end;

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

end;

then rng a' c= Funcs the carrier of H',the carrier of H' by TARSKI:def 3;
then reconsider a' = a' as Action of O,the carrier of H' by A17, FUNCT_2:4;
reconsider H = HGrWOpStr(# the carrier of H',the multF of H',a' #) as non empty HGrWOpStr of O ;
A31: H is Group-like by A6;
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;
then A32: H is Subgroup of G by A31, GROUP_2:def 5;

now

let G' be Group; :: thesis:
let a be Action of O,the carrier of G'; :: thesis:
assume A33: a = the action of H ; :: thesis:
assume A34: multMagma(# the carrier of G',the multF of G' #) = 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 & dom f = the carrier of G' & rng f c= the carrier of G' ) by FUNCT_2:def 2;
[o,(a . o)] in a' by A33, A35, FUNCT_1:8;
then consider o' being Element of O such that
A37: [o,(a . o)] = [o',((G ^ o') | the carrier of H')] ;
A38: ( o = o' & a . o = (G ^ o') | the carrier of H' ) by A37, ZFMISC_1:33;
reconsider f = f as Function of G',G' by A36, FUNCT_2:4;

now

let a', b' be Element of G'; :: thesis:
a' * b' in the carrier of H' by A34;
then A39: a' * b' in dom (id the carrier of H') by RELAT_1:71;
( a' in the carrier of H' & b' in the carrier of H' ) by A34;
then A40: ( a' in dom (id the carrier of H') & b' in dom (id the carrier of H') ) by RELAT_1:71;
reconsider a = a', b = b' as Element of H by A34;
reconsider g1 = a, g2 = b as Element of G by GROUP_2:51;
reconsider h1 = (G ^ o) . g1, h2 = (G ^ o) . g2 as Element of H by A4, A5;
A41: f . a' = ((G ^ o) * (id the carrier of H')) . a' by A36, A38, RELAT_1:94
.= (G ^ o) . ((id the carrier of H') . a') by A40, FUNCT_1:23
.= h1 by FUNCT_1:35 ;
A42: f . b' = ((G ^ o) * (id the carrier of H')) . b' by A36, A38, RELAT_1:94
.= (G ^ o) . ((id the carrier of H') . b') by A40, FUNCT_1:23
.= h2 by FUNCT_1:35 ;
thus f . (a' * b') = ((G ^ o) * (id the carrier of H')) . (a' * b') by A36, A38, RELAT_1:94
.= (G ^ o) . ((id the carrier of H') . (a' * b')) by A39, 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 . a') * (f . b') by A34, A41, A42 ; :: thesis:

end;

hence a . o is Homomorphism of G',G' 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 A6, Def5;

now

let o be Element of O; :: thesis:
o in O by A15;
then o in dom a' by FUNCT_2:def 1;
then [o,(a' . o)] in a' by FUNCT_1:8;
then consider o' being Element of O such that
A43: [o,(a' . o)] = [o',((G ^ o') | the carrier of H')] ;
( o = o' & a' . o = (G ^ o') | the carrier of H' ) by A43, ZFMISC_1:33;
hence H ^ o = (G ^ o) | the carrier of H by A15, 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 A5; :: thesis:

end;