let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)
let s1, s2 be CompositionSeries of G; :: thesis: for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)
let i be Nat; :: thesis: ( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) implies the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) )
set f1 = the_series_of_quotients_of s1;
assume A1: i in dom s1 ; :: thesis: ( not i + 1 in dom s1 or not s1 . i = s1 . (i + 1) or not s2 = Del (s1,i) or the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) )
then consider k being Nat such that
A2: len s1 = k + 1 and
A3: len (Del (s1,i)) = k by FINSEQ_3:104;
assume i + 1 in dom s1 ; :: thesis: ( not s1 . i = s1 . (i + 1) or not s2 = Del (s1,i) or the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) )
then i + 1 in Seg (len s1) by FINSEQ_1:def 3;
then A4: i + 1 <= len s1 by FINSEQ_1:1;
assume A5: s1 . i = s1 . (i + 1) ; :: thesis: ( not s2 = Del (s1,i) or the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) )
A6: i in Seg (len s1) by A1, FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then A7: 1 + 1 <= i + 1 by XREAL_1:6;
then 2 <= len s1 by A4, XXREAL_0:2;
then A8: 1 < len s1 by XXREAL_0:2;
then A9: len s1 = (len (the_series_of_quotients_of s1)) + 1 by Def33;
assume A10: s2 = Del (s1,i) ; :: thesis: the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)
then 1 + 1 <= (len s2) + 1 by A7, A4, A2, A3, XXREAL_0:2;
then A11: 1 <= len s2 by XREAL_1:6;

per cases ( len s2 = 1 or len s2 > 1 ) by A11, XXREAL_0:1;

suppose A12: len s2 = 1 ; :: thesis: the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)

then 1 in Seg (len (the_series_of_quotients_of s1)) by A10, A2, A3, A9;
then 1 in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
then A13: ex k1 being Nat st
( len (the_series_of_quotients_of s1) = k1 + 1 & len (Del ((the_series_of_quotients_of s1),1)) = k1 ) by FINSEQ_3:104;
A14: 1 <= i by A6, FINSEQ_1:1;
A15: the_series_of_quotients_of s2 = {} by A12, Def33;
i <= 1 by A10, A4, A2, A3, A12, XREAL_1:6;
then len (Del ((the_series_of_quotients_of s1),i)) = 0 by A10, A2, A3, A9, A12, A13, A14, XXREAL_0:1;
hence the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) by A15; :: thesis: verum

end;

suppose A16: len s2 > 1 ; :: thesis: the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)

( (i + 1) - 1 <= (len s1) - 1 & 1 <= i ) by A6, A4, FINSEQ_1:1, XREAL_1:9;
then i in Seg (len (the_series_of_quotients_of s1)) by A9;
then A17: i in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
then consider k1 being Nat such that
A18: len (the_series_of_quotients_of s1) = k1 + 1 and
A19: len (Del ((the_series_of_quotients_of s1),i)) = k1 by FINSEQ_3:104;

now :: thesis: for n being Nat st n in dom (Del ((the_series_of_quotients_of s1),i)) holds
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del ((the_series_of_quotients_of s1),i)) . n = H1 ./. N1

let n be Nat; :: thesis: ( n in dom (Del ((the_series_of_quotients_of s1),i)) implies for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del ((the_series_of_quotients_of s1),i)) . b₃ = b₄ ./. b₅ )
set n1 = n + 1;
assume n in dom (Del ((the_series_of_quotients_of s1),i)) ; :: thesis: for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del ((the_series_of_quotients_of s1),i)) . b₃ = b₄ ./. b₅
then A20: n in Seg (len (Del ((the_series_of_quotients_of s1),i))) by FINSEQ_1:def 3;
then A21: n <= k1 by A19, FINSEQ_1:1;
then A22: n + 1 <= k by A2, A9, A18, XREAL_1:6;
1 <= n by A20, FINSEQ_1:1;
then 1 + 1 <= n + 1 by XREAL_1:6;
then 1 <= n + 1 by XXREAL_0:2;
then n + 1 in Seg (len (the_series_of_quotients_of s1)) by A2, A9, A22;
then A23: n + 1 in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
reconsider n1 = n + 1 as Nat ;
let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st H1 = s2 . n & N1 = s2 . (n + 1) holds
(Del ((the_series_of_quotients_of s1),i)) . b₂ = b₃ ./. b₄
let N1 be normal StableSubgroup of H1; :: thesis: ( H1 = s2 . n & N1 = s2 . (n + 1) implies (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃ )
assume A24: H1 = s2 . n ; :: thesis: ( N1 = s2 . (n + 1) implies (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃ )
0 + n < 1 + n by XREAL_1:6;
then A25: n <= k by A22, XXREAL_0:2;
((len (the_series_of_quotients_of s1)) - (len (Del ((the_series_of_quotients_of s1),i)))) + (len (Del ((the_series_of_quotients_of s1),i))) > 0 + (len (Del ((the_series_of_quotients_of s1),i))) by A18, A19, XREAL_1:6;
then Seg (len (Del ((the_series_of_quotients_of s1),i))) c= Seg (len (the_series_of_quotients_of s1)) by FINSEQ_1:5;
then n in Seg (len (the_series_of_quotients_of s1)) by A20;
then A26: n in dom (the_series_of_quotients_of s1) by FINSEQ_1:def 3;
assume A27: N1 = s2 . (n + 1) ; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃

per cases ( n < i or n >= i ) ;

suppose A28: n < i ; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃

then A29: n1 <= i by NAT_1:13;

per cases ( n1 < i or n1 = i ) by A29, XXREAL_0:1;

suppose A30: n1 < i ; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃

reconsider n9 = n as Element of NAT by INT_1:3;
A31: s1 . (n9 + 1) = N1 by A10, A27, A30, FINSEQ_3:110;
s1 . n9 = H1 by A10, A24, A28, FINSEQ_3:110;
then (the_series_of_quotients_of s1) . n = H1 ./. N1 by A8, A26, A31, Def33;
hence (Del ((the_series_of_quotients_of s1),i)) . n = H1 ./. N1 by A28, FINSEQ_3:110; :: thesis: verum

end;

suppose n1 = i ; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃

then ( s1 . n = H1 & s1 . (n + 1) = N1 ) by A1, A5, A10, A2, A24, A27, A22, A28, FINSEQ_3:110, FINSEQ_3:111;
then (the_series_of_quotients_of s1) . n = H1 ./. N1 by A8, A26, Def33;
hence (Del ((the_series_of_quotients_of s1),i)) . n = H1 ./. N1 by A28, FINSEQ_3:110; :: thesis: verum

end;

end;

end;

suppose A32: n >= i ; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b₁ = b₂ ./. b₃

reconsider n19 = n1 as Element of NAT ;
( 0 + i < 1 + i & n + 1 >= i + 1 ) by A32, XREAL_1:6;
then n1 >= i by XXREAL_0:2;
then A33: s1 . (n19 + 1) = N1 by A1, A10, A2, A27, A22, FINSEQ_3:111;
s1 . n19 = H1 by A1, A10, A2, A24, A25, A32, FINSEQ_3:111;
then (the_series_of_quotients_of s1) . n1 = H1 ./. N1 by A8, A23, A33, Def33;
hence (Del ((the_series_of_quotients_of s1),i)) . n = H1 ./. N1 by A17, A18, A21, A32, FINSEQ_3:111; :: thesis: verum

end;

end;

end;

hence the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i) by A10, A2, A3, A9, A16, A18, A19, Def33; :: thesis: verum

end;

end;