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

for H1 being StableSubgroup of G

for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let H1 be StableSubgroup of G; :: thesis: for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let N1, N2 be strict StableSubgroup of H1; :: thesis: for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

reconsider S2 = the_stable_subgroup_of (N1 * N2) as StableSubgroup of G by Th11;

let N19, N29 be strict StableSubgroup of G; :: thesis: ( N1 = N19 & N2 = N29 implies N19 "\/" N29 = N1 "\/" N2 )

set S1 = the_stable_subgroup_of (N19 * N29);

set X1 = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } ;

set X2 = { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ;

A1: ( N19 "\/" N29 = the_stable_subgroup_of (N19 * N29) & N1 "\/" N2 = the_stable_subgroup_of (N1 * N2) ) by Th29;

A2: ( the carrier of (the_stable_subgroup_of (N19 * N29)) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } & the carrier of (the_stable_subgroup_of (N1 * N2)) = meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ) by Th27;

assume A3: ( N1 = N19 & N2 = N29 ) ; :: thesis: N19 "\/" N29 = N1 "\/" N2

( B = the carrier of H & N1 * N2 c= carr H ) } c= { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } ;

( B = the carrier of H & N19 * N29 c= carr H ) } c= meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } by A7, SETFAM_1:6;

( B = the carrier of H & N1 * N2 c= carr H ) } c= meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } by A2;

then the carrier of (the_stable_subgroup_of (N19 * N29)) = the carrier of S2 by A2, A8, XBOOLE_0:def 10;

hence N19 "\/" N29 = N1 "\/" N2 by A1, Lm4; :: thesis: verum

for H1 being StableSubgroup of G

for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let H1 be StableSubgroup of G; :: thesis: for N1, N2 being strict StableSubgroup of H1

for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

let N1, N2 be strict StableSubgroup of H1; :: thesis: for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds

N19 "\/" N29 = N1 "\/" N2

reconsider S2 = the_stable_subgroup_of (N1 * N2) as StableSubgroup of G by Th11;

let N19, N29 be strict StableSubgroup of G; :: thesis: ( N1 = N19 & N2 = N29 implies N19 "\/" N29 = N1 "\/" N2 )

set S1 = the_stable_subgroup_of (N19 * N29);

set X1 = { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } ;

set X2 = { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ;

A1: ( N19 "\/" N29 = the_stable_subgroup_of (N19 * N29) & N1 "\/" N2 = the_stable_subgroup_of (N1 * N2) ) by Th29;

A2: ( the carrier of (the_stable_subgroup_of (N19 * N29)) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } & the carrier of (the_stable_subgroup_of (N1 * N2)) = meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ) by Th27;

assume A3: ( N1 = N19 & N2 = N29 ) ; :: thesis: N19 "\/" N29 = N1 "\/" N2

now :: thesis: for x being object st x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } holds

x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) }

then A7:
{ B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st ( B = the carrier of H & N1 * N2 c= carr H ) } holds

x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) }

let x be object ; :: thesis: ( x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } implies x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } )

assume x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ; :: thesis: x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) }

then consider B being Subset of H1 such that

A4: x = B and

A5: ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) ;

( B = the carrier of H & N19 * N29 c= carr H ) } by A4; :: thesis: verum

end;( B = the carrier of H & N1 * N2 c= carr H ) } implies x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } )

assume x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } ; :: thesis: x in { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) }

then consider B being Subset of H1 such that

A4: x = B and

A5: ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) ;

now :: thesis: ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H )

hence
x in { B where B is Subset of G : ex H being strict StableSubgroup of G st ( B = the carrier of H & N19 * N29 c= carr H )

consider H being strict StableSubgroup of H1 such that

A6: ( B = the carrier of H & N1 * N2 c= carr H ) by A5;

reconsider H = H as strict StableSubgroup of G by Th11;

take H = H; :: thesis: ( B = the carrier of H & N19 * N29 c= carr H )

thus ( B = the carrier of H & N19 * N29 c= carr H ) by A3, A6, Th85; :: thesis: verum

end;A6: ( B = the carrier of H & N1 * N2 c= carr H ) by A5;

reconsider H = H as strict StableSubgroup of G by Th11;

take H = H; :: thesis: ( B = the carrier of H & N19 * N29 c= carr H )

thus ( B = the carrier of H & N19 * N29 c= carr H ) by A3, A6, Th85; :: thesis: verum

( B = the carrier of H & N19 * N29 c= carr H ) } by A4; :: thesis: verum

( B = the carrier of H & N1 * N2 c= carr H ) } c= { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } ;

now :: thesis: ex x being set st x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) }

then A8:
meet { B where B is Subset of G : ex H being strict StableSubgroup of G st ( B = the carrier of H & N1 * N2 c= carr H ) }

set x9 = carr H1;

reconsider x = carr H1 as set ;

take x = x; :: thesis: x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) }

( B = the carrier of H & N1 * N2 c= carr H ) } ; :: thesis: verum

end;reconsider x = carr H1 as set ;

take x = x; :: thesis: x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) }

now :: thesis: ex H being strict StableSubgroup of H1 st

( carr H1 = the carrier of H & N1 * N2 c= carr H )

hence
x in { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st ( carr H1 = the carrier of H & N1 * N2 c= carr H )

set H = (Omega). H1;

take H = (Omega). H1; :: thesis: ( carr H1 = the carrier of H & N1 * N2 c= carr H )

thus carr H1 = the carrier of H ; :: thesis: N1 * N2 c= carr H

thus N1 * N2 c= carr H ; :: thesis: verum

end;take H = (Omega). H1; :: thesis: ( carr H1 = the carrier of H & N1 * N2 c= carr H )

thus carr H1 = the carrier of H ; :: thesis: N1 * N2 c= carr H

thus N1 * N2 c= carr H ; :: thesis: verum

( B = the carrier of H & N1 * N2 c= carr H ) } ; :: thesis: verum

( B = the carrier of H & N19 * N29 c= carr H ) } c= meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st

( B = the carrier of H & N1 * N2 c= carr H ) } by A7, SETFAM_1:6;

now :: thesis: for x being object st x in the carrier of (the_stable_subgroup_of (N1 * N2)) holds

x in the carrier of (the_stable_subgroup_of (N19 * N29))

then
meet { B where B is Subset of H1 : ex H being strict StableSubgroup of H1 st x in the carrier of (the_stable_subgroup_of (N19 * N29))

let x be object ; :: thesis: ( x in the carrier of (the_stable_subgroup_of (N1 * N2)) implies x in the carrier of (the_stable_subgroup_of (N19 * N29)) )

assume A9: x in the carrier of (the_stable_subgroup_of (N1 * N2)) ; :: thesis: x in the carrier of (the_stable_subgroup_of (N19 * N29))

the_stable_subgroup_of (N1 * N2) is Subgroup of H1 by Def7;

then the carrier of (the_stable_subgroup_of (N1 * N2)) c= the carrier of H1 by GROUP_2:def 5;

then reconsider g = x as Element of H1 by A9;

g in the_stable_subgroup_of (N1 * N2) by A9, STRUCT_0:def 5;

then consider F being FinSequence of the carrier of H1, I being FinSequence of INT , C being Subset of H1 such that

A10: C = the_stable_subset_generated_by ((N1 * N2), the action of H1) and

A11: len F = len I and

A12: rng F c= C and

A13: Product (F |^ I) = g by Th24;

then A24: rng F c= the_stable_subset_generated_by ((N19 * N29), the action of G) by A10, A12;

reconsider g = g as Element of G by Th2;

H1 is Subgroup of G by Def7;

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

then rng F c= the carrier of G ;

then reconsider F = F as FinSequence of the carrier of G by FINSEQ_1:def 4;

Product (F |^ I) = g by A11, A13, Th83;

then A25: g in the_stable_subgroup_of (N19 * N29) by A11, A24, Th24;

assume not x in the carrier of (the_stable_subgroup_of (N19 * N29)) ; :: thesis: contradiction

hence contradiction by A25, STRUCT_0:def 5; :: thesis: verum

end;assume A9: x in the carrier of (the_stable_subgroup_of (N1 * N2)) ; :: thesis: x in the carrier of (the_stable_subgroup_of (N19 * N29))

the_stable_subgroup_of (N1 * N2) is Subgroup of H1 by Def7;

then the carrier of (the_stable_subgroup_of (N1 * N2)) c= the carrier of H1 by GROUP_2:def 5;

then reconsider g = x as Element of H1 by A9;

g in the_stable_subgroup_of (N1 * N2) by A9, STRUCT_0:def 5;

then consider F being FinSequence of the carrier of H1, I being FinSequence of INT , C being Subset of H1 such that

A10: C = the_stable_subset_generated_by ((N1 * N2), the action of H1) and

A11: len F = len I and

A12: rng F c= C and

A13: Product (F |^ I) = g by Th24;

now :: thesis: for x being object st x in the_stable_subset_generated_by ((N1 * N2), the action of H1) holds

x in the_stable_subset_generated_by ((N19 * N29), the action of G)

then
the_stable_subset_generated_by ((N1 * N2), the action of H1) c= the_stable_subset_generated_by ((N19 * N29), the action of G)
;x in the_stable_subset_generated_by ((N19 * N29), the action of G)

N2 is Subgroup of H1
by Def7;

then 1_ H1 in N2 by GROUP_2:46;

then A14: 1_ H1 in carr N2 by STRUCT_0:def 5;

let x be object ; :: thesis: ( x in the_stable_subset_generated_by ((N1 * N2), the action of H1) implies x in the_stable_subset_generated_by ((N19 * N29), the action of G) )

assume A15: x in the_stable_subset_generated_by ((N1 * N2), the action of H1) ; :: thesis: x in the_stable_subset_generated_by ((N19 * N29), the action of G)

then reconsider a = x as Element of H1 ;

N1 is Subgroup of H1 by Def7;

then 1_ H1 in N1 by GROUP_2:46;

then A16: 1_ H1 in carr N1 by STRUCT_0:def 5;

1_ H1 = (1_ H1) * (1_ H1) by GROUP_1:def 4;

then A17: 1_ H1 in (carr N1) * (carr N2) by A16, A14;

then consider F being FinSequence of O, h being Element of N1 * N2 such that

A18: (Product (F, the action of H1)) . h = a by A15, Lm30;

H1 is Subgroup of G by Def7;

then A19: the carrier of H1 c= the carrier of G by GROUP_2:def 5;

then reconsider a = a as Element of G ;

A20: h in N1 * N2 by A17;

reconsider h = h as Element of N19 * N29 by A3, Th85;

then A23: (Product (F, the action of G)) . h = a by A18, A20, FUNCT_1:49;

not N19 * N29 is empty by A3, A20, Th85;

hence x in the_stable_subset_generated_by ((N19 * N29), the action of G) by A23, Lm30; :: thesis: verum

end;then 1_ H1 in N2 by GROUP_2:46;

then A14: 1_ H1 in carr N2 by STRUCT_0:def 5;

let x be object ; :: thesis: ( x in the_stable_subset_generated_by ((N1 * N2), the action of H1) implies x in the_stable_subset_generated_by ((N19 * N29), the action of G) )

assume A15: x in the_stable_subset_generated_by ((N1 * N2), the action of H1) ; :: thesis: x in the_stable_subset_generated_by ((N19 * N29), the action of G)

then reconsider a = x as Element of H1 ;

N1 is Subgroup of H1 by Def7;

then 1_ H1 in N1 by GROUP_2:46;

then A16: 1_ H1 in carr N1 by STRUCT_0:def 5;

1_ H1 = (1_ H1) * (1_ H1) by GROUP_1:def 4;

then A17: 1_ H1 in (carr N1) * (carr N2) by A16, A14;

then consider F being FinSequence of O, h being Element of N1 * N2 such that

A18: (Product (F, the action of H1)) . h = a by A15, Lm30;

H1 is Subgroup of G by Def7;

then A19: the carrier of H1 c= the carrier of G by GROUP_2:def 5;

then reconsider a = a as Element of G ;

A20: h in N1 * N2 by A17;

reconsider h = h as Element of N19 * N29 by A3, Th85;

now :: thesis: for o being Element of O

for f1 being Function of the carrier of H1, the carrier of H1

for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

f1 = f2 | the carrier of H1

then
Product (F, the action of H1) = (Product (F, the action of G)) | the carrier of H1
by A19, Th84;for f1 being Function of the carrier of H1, the carrier of H1

for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

f1 = f2 | the carrier of H1

let o be Element of O; :: thesis: for f1 being Function of the carrier of H1, the carrier of H1

for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

b_{4} = b_{5} | the carrier of H1

let f1 be Function of the carrier of H1, the carrier of H1; :: thesis: for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

b_{3} = b_{4} | the carrier of H1

let f2 be Function of the carrier of G, the carrier of G; :: thesis: ( f1 = the action of H1 . o & f2 = the action of G . o implies b_{2} = b_{3} | the carrier of H1 )

assume that

A21: f1 = the action of H1 . o and

A22: f2 = the action of G . o ; :: thesis: b_{2} = b_{3} | the carrier of H1

end;for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

b

let f1 be Function of the carrier of H1, the carrier of H1; :: thesis: for f2 being Function of the carrier of G, the carrier of G st f1 = the action of H1 . o & f2 = the action of G . o holds

b

let f2 be Function of the carrier of G, the carrier of G; :: thesis: ( f1 = the action of H1 . o & f2 = the action of G . o implies b

assume that

A21: f1 = the action of H1 . o and

A22: f2 = the action of G . o ; :: thesis: b

per cases
( o in O or not o in O )
;

end;

suppose
o in O
; :: thesis: b_{2} = b_{3} | the carrier of H1

then
( H1 ^ o = f1 & G ^ o = f2 )
by A21, A22, Def6;

hence f1 = f2 | the carrier of H1 by Def7; :: thesis: verum

end;hence f1 = f2 | the carrier of H1 by Def7; :: thesis: verum

suppose
not o in O
; :: thesis: b_{2} = b_{3} | the carrier of H1

then
not o in dom the action of H1
;

hence f1 = f2 | the carrier of H1 by A21, FUNCT_1:def 2; :: thesis: verum

end;hence f1 = f2 | the carrier of H1 by A21, FUNCT_1:def 2; :: thesis: verum

then A23: (Product (F, the action of G)) . h = a by A18, A20, FUNCT_1:49;

not N19 * N29 is empty by A3, A20, Th85;

hence x in the_stable_subset_generated_by ((N19 * N29), the action of G) by A23, Lm30; :: thesis: verum

then A24: rng F c= the_stable_subset_generated_by ((N19 * N29), the action of G) by A10, A12;

reconsider g = g as Element of G by Th2;

H1 is Subgroup of G by Def7;

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

then rng F c= the carrier of G ;

then reconsider F = F as FinSequence of the carrier of G by FINSEQ_1:def 4;

Product (F |^ I) = g by A11, A13, Th83;

then A25: g in the_stable_subgroup_of (N19 * N29) by A11, A24, Th24;

assume not x in the carrier of (the_stable_subgroup_of (N19 * N29)) ; :: thesis: contradiction

hence contradiction by A25, STRUCT_0:def 5; :: thesis: verum

( B = the carrier of H & N1 * N2 c= carr H ) } c= meet { B where B is Subset of G : ex H being strict StableSubgroup of G st

( B = the carrier of H & N19 * N29 c= carr H ) } by A2;

then the carrier of (the_stable_subgroup_of (N19 * N29)) = the carrier of S2 by A2, A8, XBOOLE_0:def 10;

hence N19 "\/" N29 = N1 "\/" N2 by A1, Lm4; :: thesis: verum