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
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 )
}
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 ) ;
now :: thesis: 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;
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 )
}
by A4; :: thesis: verum
end;
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 ) } 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 )
}
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 )
}

now :: thesis: 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;
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: verum
end;
then A8: 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 )
}
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 ;
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))
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 ;
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)
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 ;
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 ;
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 ;
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
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
b4 = b5 | 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
b3 = b4 | 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 b2 = b3 | the carrier of H1 )
assume that
A21: f1 = the action of H1 . o and
A22: f2 = the action of G . o ; :: thesis: b2 = b3 | the carrier of H1
per cases ( o in O or not o in O ) ;
suppose o in O ; :: thesis: b2 = b3 | the carrier of H1
then ( H1 ^ o = f1 & G ^ o = f2 ) by ;
hence f1 = f2 | the carrier of H1 by Def7; :: thesis: verum
end;
suppose not o in O ; :: thesis: b2 = b3 | the carrier of H1
then not o in dom the action of H1 ;
hence f1 = f2 | the carrier of H1 by ; :: thesis: verum
end;
end;
end;
then Product (F, the action of H1) = (Product (F, the action of G)) | the carrier of H1 by ;
then A23: (Product (F, the action of G)) . h = a by ;
not N19 * N29 is empty by ;
hence x in the_stable_subset_generated_by ((N19 * N29), the action of G) by ; :: thesis: verum
end;
then the_stable_subset_generated_by ((N1 * N2), the action of H1) c= the_stable_subset_generated_by ((N19 * N29), the action of G) ;
then A24: rng F c= the_stable_subset_generated_by ((N19 * N29), the action of G) by ;
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 ;
then A25: g in the_stable_subgroup_of (N19 * N29) by ;
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;
then 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 & N19 * N29 c= carr H )
}
by A2;
then the carrier of (the_stable_subgroup_of (N19 * N29)) = the carrier of S2 by ;
hence N19 "\/" N29 = N1 "\/" N2 by ; :: thesis: verum