(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;
then reconsider l99 = (len s2) - 1 as Element of NAT by INT_1:3;
(len s2) + 1 > 1 + 1 by A2, XREAL_1:6;
then len s2 >= 2 by NAT_1:13;
then A3: (len s2) - 1 >= 2 - 1 by XREAL_1:9;
(len s1) - 1 > 1 - 1 by A1, XREAL_1:9;
then reconsider l9 = (len s1) - 1 as Element of NAT by INT_1:3;
defpred S₁[ set , object ] means for i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( $1 = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies $2 = H1 "\/" (H2 /\ H3) ) & ( $1 = (((len s1) - 1) * ((len s2) - 1)) + 1 implies $2 = (1). G ) );
(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;
then A4: l99 / l99 = 1 by XCMPLX_1:60;
(len s1) + 1 > 1 + 1 by A1, XREAL_1:6;
then len s1 >= 2 by NAT_1:13;
then A5: (len s1) - 1 >= 2 - 1 by XREAL_1:9;
then A6: (((len s1) - 1) * ((len s2) - 1)) + 1 >= 0 + 1 by A3, XREAL_1:6;
reconsider l = (((len s1) - 1) * ((len s2) - 1)) + 1 as Element of NAT by A5, A3, INT_1:3;
A7: 1 in Seg l by A6;
A8: for k being Nat st k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
for i, j being Nat holds
( not k = ((i - 1) * ((len s2) - 1)) + j or not 1 <= i or not i <= (len s1) - 1 or not 1 <= j or not j <= (len s2) - 1 )

let k be Nat; :: thesis:
assume A9: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:
assume ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis:
then consider i, j being Nat such that
A10: k = ((i - 1) * ((len s2) - 1)) + j and
A11: 1 <= i and
A12: i <= (len s1) - 1 and
A13: 1 <= j and
A14: j <= (len s2) - 1 ;
set i9 = i - 1;
i - 1 >= 1 - 1 by A11, XREAL_1:9;
then reconsider i9 = i - 1 as Element of NAT by INT_1:3;
A15: 1 mod l99 = ((l9 * l99) + 1) mod l99 by NAT_D:21
.= ((i9 * l99) + j) mod l99 by A9, A10
.= j mod l99 by NAT_D:21 ;
j = 1

per cases ;

suppose A16: j = l99 ; :: thesis:

assume j <> 1 ; :: thesis:
then 1 < l99 by A13, A16, XXREAL_0:1;
then 1 = j mod l99 by A15, NAT_D:24;
hence contradiction by A16, NAT_D:25; :: thesis:

end;

suppose j <> l99 ; :: thesis:

then j < l99 by A14, XXREAL_0:1;
then A17: j mod l99 = j by NAT_D:24;

per cases ;

suppose 1 = l99 ; :: thesis:

hence j = 1 by A13, A14, XXREAL_0:1; :: thesis:

end;

suppose A18: 1 <> l99 ; :: thesis:

1 <= l99 by A13, A14, XXREAL_0:2;
then 1 < l99 by A18, XXREAL_0:1;
hence j = 1 by A15, A17, NAT_D:24; :: thesis:

end;

then A19: l9 * (l99 / l99) = (i9 * l99) / l99 by A9, A10, XCMPLX_1:74;
l99 / l99 = 1 by A13, A14, XCMPLX_1:60;
then A20: l9 * 1 = i9 * 1 by A19, XCMPLX_1:74;
(- 1) + i < 0 + i by XREAL_1:6;
hence contradiction by A12, A20; :: thesis:

end;

A21: for k being Nat st k in Seg l holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis:
assume A22: k in Seg l ; :: thesis:

per cases by A1, A2, A22, Lm44;

suppose A23: ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis:

then consider i, j being Nat such that
A24: k = ((i - 1) * ((len s2) - 1)) + j and
A25: 1 <= i and
A26: i <= (len s1) - 1 and
A27: ( 1 <= j & j <= (len s2) - 1 ) ;
reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A25, A26, A27, Th111;
take x = H1 "\/" (H2 /\ H3); :: thesis:

now :: thesis:

let i1, j1 be Nat; :: thesis:
let H1, H2, H3 be StableSubgroup of G; :: thesis:
thus ( k = ((i1 - 1) * ((len s2) - 1)) + j1 & 1 <= i1 & i1 <= (len s1) - 1 & 1 <= j1 & j1 <= (len s2) - 1 & H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 implies x = H1 "\/" (H2 /\ H3) ) :: thesis:

proof

assume that
A28: k = ((i1 - 1) * ((len s2) - 1)) + j1 and
A29: 1 <= i1 and
i1 <= (len s1) - 1 and
A30: ( 1 <= j1 & j1 <= (len s2) - 1 ) ; :: thesis:
assume A31: ( H1 = s1 . (i1 + 1) & H2 = s1 . i1 & H3 = s2 . j1 ) ; :: thesis:
i = i1 by A2, A24, A25, A27, A28, A29, A30, Lm45;
hence x = H1 "\/" (H2 /\ H3) by A24, A28, A31; :: thesis:

end;

assume k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:
hence x = (1). G by A8, A23; :: thesis:

end;

hence S₁[k,x] ; :: thesis:

end;

suppose A32: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:

take (1). G ; :: thesis:
thus S₁[k, (1). G] by A8, A32; :: thesis:

end;

consider f being FinSequence such that
A33: ( dom f = Seg l & ( for k being Nat st k in Seg l holds
S₁[k,f . k] ) ) from FINSEQ_1:sch 1(A21);
for k being Nat st k in dom f holds
f . k in the_stable_subgroups_of G

proof

let k be Nat; :: thesis:
assume A34: k in dom f ; :: thesis:
then A35: for i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) ) by A33;

per cases by A1, A2, A33, A34, Lm44;

suppose ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ; :: thesis:

then consider i, j being Nat such that
A36: k = ((i - 1) * ((len s2) - 1)) + j and
A37: ( 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) ;
reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A37, Th111;
f . k = H1 "\/" (H2 /\ H3) by A33, A34, A36, A37;
hence f . k in the_stable_subgroups_of G by Def11; :: thesis:

end;

suppose k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:

hence f . k in the_stable_subgroups_of G by A35, Def11; :: thesis:

end;

then reconsider f = f as FinSequence of the_stable_subgroups_of G by FINSEQ_2:12;
l in Seg l by A6;
then S₁[l,f . l] by A33;
then A38: f . (len f) = (1). G by A33, FINSEQ_1:def 3;
A39: for i being Nat
for s1 being CompositionSeries of G
for H being GroupWithOperators of O st 1 <= i & i <= (len s1) - 1 & H = s1 . i holds
s1 . (i + 1) is normal StableSubgroup of H

proof

let i be Nat; :: thesis:
let s1 be CompositionSeries of G; :: thesis:
let H be GroupWithOperators of O; :: thesis:
assume that
A40: 1 <= i and
A41: i <= (len s1) - 1 ; :: thesis:
A42: 0 + i <= 1 + i by XREAL_1:6;
A43: i + 1 <= ((len s1) - 1) + 1 by A41, XREAL_1:6;
then i <= len s1 by A42, XXREAL_0:2;
then i in Seg (len s1) by A40;
then A44: i in dom s1 by FINSEQ_1:def 3;
reconsider H1 = s1 . i, H2 = s1 . (i + 1) as StableSubgroup of G by A40, A41, Th111;
assume A45: H = s1 . i ; :: thesis:
1 <= i + 1 by A40, A42, XXREAL_0:2;
then i + 1 in Seg (len s1) by A43;
then i + 1 in dom s1 by FINSEQ_1:def 3;
then H2 is normal StableSubgroup of H1 by A44, Def28;
hence s1 . (i + 1) is normal StableSubgroup of H by A45; :: thesis:

end;

A46: for k being Nat st k in dom f & k + 1 in dom f holds
for H1, H2 being StableSubgroup of G st H1 = f . k & H2 = f . (k + 1) holds
H2 is normal StableSubgroup of H1

proof

let k be Nat; :: thesis:
assume A47: k in dom f ; :: thesis:
set k9 = k + 1;
assume A48: k + 1 in dom f ; :: thesis:
then k + 1 <= l by A33, FINSEQ_1:1;
then k <> l by NAT_1:13;
then consider i, j being Nat such that
A49: k = ((i - 1) * ((len s2) - 1)) + j and
A50: 1 <= i and
A51: i <= (len s1) - 1 and
A52: 1 <= j and
A53: j <= (len s2) - 1 by A1, A2, A33, A47, Lm44;
reconsider H19 = s1 . (i + 1), H29 = s1 . i, H39 = s2 . j as strict StableSubgroup of G by A50, A51, A52, A53, Th111;
A54: f . k = H19 "\/" (H29 /\ H39) by A33, A47, A49, A50, A51, A52, A53;
let H1, H2 be StableSubgroup of G; :: thesis:
assume A55: H1 = f . k ; :: thesis:
A56: H19 is normal StableSubgroup of H29 by A39, A50, A51;
assume A57: H2 = f . (k + 1) ; :: thesis:

per cases ;

suppose A58: j <> (len s2) - 1 ; :: thesis:

reconsider j9 = j + 1 as Nat ;
j < (len s2) - 1 by A53, A58, XXREAL_0:1;
then A59: j9 <= (len s2) - 1 by INT_1:7;
reconsider H399 = s2 . j9 as strict StableSubgroup of G by A52, A53, Th111;
0 + j <= 1 + j by XREAL_1:6;
then A60: 1 <= j9 by A52, XXREAL_0:2;
A61: H399 is normal StableSubgroup of H39 by A39, A52, A53;
k + 1 = ((i - 1) * ((len s2) - 1)) + j9 by A49;
then H2 = H19 "\/" (H29 /\ H399) by A33, A48, A50, A51, A57, A59, A60;
hence H2 is normal StableSubgroup of H1 by A55, A56, A54, A61, Th92; :: thesis:

end;

suppose A62: j = (len s2) - 1 ; :: thesis:

per cases ;

suppose A63: i <> (len s1) - 1 ; :: thesis:

set i9 = i + 1;
A64: 0 + (i + 1) <= 1 + (i + 1) by XREAL_1:6;
set j9 = 1;
H19 is StableSubgroup of H1 by A55, A54, Th35;
then H19 is Subgroup of H1 by Def7;
then A65: the carrier of H19 c= the carrier of H1 by GROUP_2:def 5;
1 + 1 <= i + 1 by A50, XREAL_1:6;
then A66: 1 <= i + 1 by XXREAL_0:2;
i < l9 by A51, A63, XXREAL_0:1;
then A67: i + 1 <= l9 by NAT_1:13;
then A68: (i + 1) + 1 <= ((len s1) - 1) + 1 by XREAL_1:6;
then i + 1 <= len s1 by A64, XXREAL_0:2;
then i + 1 in Seg (len s1) by A66;
then A69: i + 1 in dom s1 by FINSEQ_1:def 3;
(len s2) - 1 > 1 - 1 by A2, XREAL_1:9;
then A70: l99 >= 0 + 1 by NAT_1:13;
then reconsider H199 = s1 . ((i + 1) + 1), H299 = s1 . (i + 1), H399 = s2 . 1 as strict StableSubgroup of G by A67, A66, Th111;
1 <= (i + 1) + 1 by A66, A64, XXREAL_0:2;
then (i + 1) + 1 in Seg (len s1) by A68;
then (i + 1) + 1 in dom s1 by FINSEQ_1:def 3;
then A71: H199 is normal StableSubgroup of H299 by A69, Def28;

now :: thesis:

let x be object ; :: thesis:
H299 is Subgroup of G by Def7;
then A72: the carrier of H299 c= the carrier of G by GROUP_2:def 5;
assume x in the carrier of H299 ; :: thesis:
hence x in the carrier of ((Omega). G) by A72; :: thesis:

end;

then the carrier of H299 c= the carrier of ((Omega). G) ;
then A73: the carrier of H299 = the carrier of H299 /\ the carrier of ((Omega). G) by XBOOLE_1:28;
A74: H399 = (Omega). G by Def28;
k + 1 = (((i + 1) - 1) * ((len s2) - 1)) + 1 by A49, A62;
then H2 = H199 "\/" (H299 /\ H399) by A33, A48, A57, A67, A66, A70;
then H2 = H199 "\/" H299 by A74, A73, Th18;
then A75: H2 = H19 by A71, Th36;
H29 /\ H39 is StableSubgroup of H29 by Lm33;
then A76: H1 is StableSubgroup of H29 by A55, A56, A54, Th37;
then A77: H1 is Subgroup of H29 by Def7;

now :: thesis:

let H9 be strict Subgroup of H1; :: thesis:
assume A78: H9 = multMagma(# the carrier of H2, the multF of H2 #) ; :: thesis:

now :: thesis:

let a be Element of H1; :: thesis:
reconsider a9 = a as Element of H29 by A76, Th2;

now :: thesis:

reconsider H1s9 = multMagma(# the carrier of H19, the multF of H19 #) as normal Subgroup of H29 by A56, Lm6;
let x be object ; :: thesis:
assume x in a * H9 ; :: thesis:
then consider b being Element of H1 such that
A79: x = a * b and
A80: b in H9 by GROUP_2:103;
set b9 = b;
A81: H1 is Subgroup of H29 by A76, Def7;
then reconsider b9 = b as Element of H29 by GROUP_2:42;
x = a9 * b9 by A79, A81, GROUP_2:43;
then ( a9 * H1s9 c= H1s9 * a9 & x in a9 * H1s9 ) by A75, A78, A80, GROUP_2:103, GROUP_3:118;
then consider b99 being Element of H29 such that
A82: x = b99 * a9 and
A83: b99 in H1s9 by GROUP_2:104;
b99 in the carrier of H19 by A83, STRUCT_0:def 5;
then reconsider b99 = b99 as Element of H1 by A65;
x = b99 * a by A77, A82, GROUP_2:43;
hence x in H9 * a by A75, A78, A83, GROUP_2:104; :: thesis:

end;

hence a * H9 c= H9 * a ; :: thesis:

end;

hence H9 is normal by GROUP_3:118; :: thesis:

end;

hence H2 is normal StableSubgroup of H1 by A55, A54, A75, Def10, Th35; :: thesis:

end;

suppose i = (len s1) - 1 ; :: thesis:

then H2 = (1). G by A33, A48, A49, A57, A62
.= (1). H1 by Th15 ;
hence H2 is normal StableSubgroup of H1 ; :: thesis:

end;

( (len s1) - 1 > 1 - 1 & (len s2) - 1 > 1 - 1 ) by A1, A2, XREAL_1:9;
then ((len s1) - 1) * ((len s2) - 1) > 0 * ((len s2) - 1) by XREAL_1:68;
then 1 <> l ;
then consider i, j being Nat such that
A84: 1 = ((i - 1) * ((len s2) - 1)) + j and
A85: 1 <= i and
A86: i <= (len s1) - 1 and
A87: 1 <= j and
A88: j <= (len s2) - 1 by A1, A2, A7, Lm44;
set i9 = i - 1;
i - 1 >= 1 - 1 by A85, XREAL_1:9;
then reconsider i9 = i - 1 as Element of NAT by INT_1:3;
reconsider H1 = s1 . (i + 1), H2 = s1 . i, H3 = s2 . j as StableSubgroup of G by A85, A86, A87, A88, Th111;
1 mod l99 = ((i9 * l99) + j) mod l99 by A84;
then A89: 1 mod l99 = j mod l99 by NAT_D:21;
A90: j = 1

proof

per cases ;

suppose l99 = 1 ; :: thesis:

hence j = 1 by A87, A88, XXREAL_0:1; :: thesis:

end;

suppose l99 <> 1 ; :: thesis:

then 1 < l99 by A3, XXREAL_0:1;
then A91: 1 = j mod l99 by A89, NAT_D:14;
then j <> l99 by NAT_D:25;
then l99 > j by A88, XXREAL_0:1;
hence j = 1 by A91, NAT_D:24; :: thesis:

end;

then A92: H3 = (Omega). G by Def28;
(i9 * l99) / l99 = 0 / l99 by A84, A90;
then i9 * 1 = 0 by A4, XCMPLX_1:74;
then A93: H2 = (Omega). G by Def28;
f . 1 = H1 "\/" (H2 /\ H3) by A33, A7, A84, A85, A86, A87, A88;
then f . 1 = H1 "\/" ((Omega). G) by A93, A92, Th19;
then f . 1 = (Omega). G by Th34;
then reconsider f = f as CompositionSeries of G by A38, A46, Def28;
take f ; :: thesis:
let k, i, j be Nat; :: thesis:
let H1, H2, H3 be StableSubgroup of G; :: thesis:
A94: for k, i, j being Nat st k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
k in Seg l

proof

let k, i, j be Nat; :: thesis:
assume A95: k = ((i - 1) * ((len s2) - 1)) + j ; :: thesis:
assume that
A96: 1 <= i and
A97: i <= (len s1) - 1 ; :: thesis:
assume that
A98: 1 <= j and
A99: j <= (len s2) - 1 ; :: thesis:
i - 1 <= l9 - 1 by A97, XREAL_1:9;
then (i - 1) * l99 <= (l9 - 1) * l99 by XREAL_1:64;
then ( 0 + (l9 * l99) <= 1 + (l9 * l99) & k <= ((l9 * l99) - (1 * l99)) + l99 ) by A95, A99, XREAL_1:7;
then A100: k <= (((len s1) - 1) * ((len s2) - 1)) + 1 by XXREAL_0:2;
1 - 1 <= i - 1 by A96, XREAL_1:9;
then 0 + 1 <= ((i - 1) * ((len s2) - 1)) + j by A3, A98, XREAL_1:7;
hence k in Seg l by A95, A100; :: thesis:

end;

now :: thesis:

assume that
A101: ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) and
A102: ( H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j ) ; :: thesis:
k in Seg l by A94, A101;
hence f . k = H1 "\/" (H2 /\ H3) by A33, A101, A102; :: thesis:

end;

hence ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies f . k = H1 "\/" (H2 /\ H3) ) ; :: thesis:

now :: thesis:

assume A103: k = (((len s1) - 1) * ((len s2) - 1)) + 1 ; :: thesis:
then k in Seg l by A6;
hence f . k = (1). G by A33, A103; :: thesis:

end;

hence ( ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies f . k = (1). G ) & len f = (((len s1) - 1) * ((len s2) - 1)) + 1 ) by A33, FINSEQ_1:def 3; :: thesis: