let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let H1 be StableSubgroup of G; :: thesis:
let N1, N2 be strict StableSubgroup of H1; :: thesis:
let N1', N2' be strict StableSubgroup of G; :: thesis:
assume A1: ( N1 = N1' & N2 = N2' ) ; :: thesis:
A2: N1' "\/" N2' = the_stable_subgroup_of (N1' * N2') by Th29;
A3: N1 "\/" N2 = the_stable_subgroup_of (N1 * N2) by Th29;
set S1 = the_stable_subgroup_of (N1' * N2');
reconsider S2 = the_stable_subgroup_of (N1 * N2) as StableSubgroup of G by Th11;
set X1 = { 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 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 ) } ;

A4: now

set x' = carr H1;
reconsider x = carr H1 as set ;
take x = x; :: thesis:

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

end;

hence 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:

end;

A5: the carrier of (the_stable_subgroup_of (N1' * N2')) = 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 ) } by Th27;
A6: 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;

let x be set ; :: thesis:
assume A7: x in the carrier of (the_stable_subgroup_of (N1 * N2)) ; :: thesis:
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 A7;
g in the_stable_subgroup_of (N1 * N2) by A7, 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
A8: ( C = the_stable_subset_generated_by (N1 * N2),the action of H1 & len F = len I & rng F c= C & Product (F |^ I) = g ) by Th24;
reconsider g = g as Element of G by Th2;

let x be set ; :: thesis:
assume A9: x in the_stable_subset_generated_by (N1 * N2),the action of H1 ; :: thesis:
then reconsider a = x as Element of H1 ;
( N1 is Subgroup of H1 & N2 is Subgroup of H1 ) by Def7;
then ( 1_ H1 in N1 & 1_ H1 in N2 ) by GROUP_2:55;
then ( 1_ H1 in carr N1 & 1_ H1 in carr N2 & 1_ H1 = (1_ H1) * (1_ H1) ) by GROUP_1:def 5, STRUCT_0:def 5;
then A10: 1_ H1 in (carr N1) * (carr N2) ;
then consider F being FinSequence of O, h being Element of N1 * N2 such that
A11: (Product F,the action of H1) . h = a by A9, Lm31;

A12: now

let o be Element of O; :: thesis:
let f1 be Function of the carrier of H1,the carrier of H1; :: thesis:
let f2 be Function of the carrier of G,the carrier of G; :: thesis:
assume A13: ( f1 = the action of H1 . o & f2 = the action of G . o ) ; :: thesis:

per cases ;

suppose o in O ; :: thesis:

then ( H1 ^ o = f1 & G ^ o = f2 ) by A13, Def6;
hence f1 = f2 | the carrier of H1 by Def7; :: thesis:

end;

suppose not o in O ; :: thesis:

then ( not o in dom the action of H1 & not o in dom the action of G ) ;
hence f1 = f2 | the carrier of H1 by A13, FUNCT_1:def 4; :: thesis:

end;

H1 is Subgroup of G by Def7;
then A14: the carrier of H1 c= the carrier of G by GROUP_2:def 5;
then A15: Product F,the action of H1 = (Product F,the action of G) | the carrier of H1 by A12, Th84;
A16: h in N1 * N2 by A10;
reconsider a = a as Element of G by A14, TARSKI:def 3;
reconsider h = h as Element of N1' * N2' by A1, Th85;
( (Product F,the action of G) . h = a & not N1' * N2' is empty ) by A1, A11, A15, A16, Th85, FUNCT_1:72;
hence x in the_stable_subset_generated_by (N1' * N2'),the action of G by Lm31; :: thesis:

end;

then the_stable_subset_generated_by (N1 * N2),the action of H1 c= the_stable_subset_generated_by (N1' * N2'),the action of G by TARSKI:def 3;
then A17: rng F c= the_stable_subset_generated_by (N1' * N2'),the action of G by A8, XBOOLE_1:1;
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 by XBOOLE_1:1;
then reconsider F = F as FinSequence of the carrier of G by FINSEQ_1:def 4;
Product (F |^ I) = g by A8, Th83;
then A18: g in the_stable_subgroup_of (N1' * N2') by A8, A17, Th24;
assume not x in the carrier of (the_stable_subgroup_of (N1' * N2')) ; :: thesis:
hence contradiction by A18, STRUCT_0:def 5; :: thesis:

end;

then A19: 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 ) } c= 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 ) } by A5, A6, TARSKI:def 3;

let x be set ; :: thesis:
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:
then consider B being Subset of H1 such that
A20: ( x = B & ex H being strict StableSubgroup of H1 st
( B = the carrier of H & N1 * N2 c= carr H ) ) ;

consider H being strict StableSubgroup of H1 such that
A21: ( B = the carrier of H & N1 * N2 c= carr H ) by A20;
reconsider H = H as strict StableSubgroup of G by Th11;
take H = H; :: thesis:
thus ( B = the carrier of H & N1' * N2' c= carr H ) by A1, A21, Th85; :: thesis:

end;

hence x in { 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 ) } by A20; :: thesis:

end;

then { 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 ) } c= { 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 ) } by TARSKI:def 3;
then 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 ) } 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 A4, SETFAM_1:7;
then the carrier of (the_stable_subgroup_of (N1' * N2')) = the carrier of S2 by A5, A6, A19, XBOOLE_0:def 10;
hence N1' "\/" N2' = N1 "\/" N2 by A2, A3, Lm5; :: thesis: