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 (,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 (,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 (,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 (,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 (,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 (,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 (,i) )
A6: i in Seg (len s1) by ;
then 1 <= i by FINSEQ_1:1;
then A7: 1 + 1 <= i + 1 by XREAL_1:6;
then 2 <= len s1 by ;
then A8: 1 < len s1 by XXREAL_0:2;
then A9: len s1 = () + 1 by Def33;
assume A10: s2 = Del (s1,i) ; :: thesis:
then 1 + 1 <= (len s2) + 1 by ;
then A11: 1 <= len s2 by XREAL_1:6;
per cases ( len s2 = 1 or len s2 > 1 ) by ;
suppose A12: len s2 = 1 ; :: thesis:
end;
suppose A16: len s2 > 1 ; :: thesis:
( (i + 1) - 1 <= (len s1) - 1 & 1 <= i ) by ;
then i in Seg () by A9;
then A17: i in dom by FINSEQ_1:def 3;
then consider k1 being Nat such that
A18: len = k1 + 1 and
A19: len (Del (,i)) = k1 by FINSEQ_3:104;
now :: thesis: for n being Nat st n in dom (Del (,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 (,i)) . n = H1 ./. N1
let n be Nat; :: thesis: ( n in dom (Del (,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 (,i)) . b3 = b4 ./. b5 )

set n1 = n + 1;
assume n in dom (Del (,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 (,i)) . b3 = b4 ./. b5

then A20: n in Seg (len (Del (,i))) by FINSEQ_1:def 3;
then A21: n <= k1 by ;
then A22: n + 1 <= k by ;
1 <= n by ;
then 1 + 1 <= n + 1 by XREAL_1:6;
then 1 <= n + 1 by XXREAL_0:2;
then n + 1 in Seg () by A2, A9, A22;
then A23: n + 1 in dom 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 (,i)) . b2 = b3 ./. b4

let N1 be normal StableSubgroup of H1; :: thesis: ( H1 = s2 . n & N1 = s2 . (n + 1) implies (Del (,i)) . b1 = b2 ./. b3 )
assume A24: H1 = s2 . n ; :: thesis: ( N1 = s2 . (n + 1) implies (Del (,i)) . b1 = b2 ./. b3 )
0 + n < 1 + n by XREAL_1:6;
then A25: n <= k by ;
((len ) - (len (Del (,i)))) + (len (Del (,i))) > 0 + (len (Del (,i))) by ;
then Seg (len (Del (,i))) c= Seg () by FINSEQ_1:5;
then n in Seg () by A20;
then A26: n in dom by FINSEQ_1:def 3;
assume A27: N1 = s2 . (n + 1) ; :: thesis: (Del (,i)) . b1 = b2 ./. b3
per cases ( n < i or n >= i ) ;
suppose A28: n < i ; :: thesis: (Del (,i)) . b1 = b2 ./. b3
then A29: n1 <= i by NAT_1:13;
per cases ( n1 < i or n1 = i ) by ;
suppose A30: n1 < i ; :: thesis: (Del (,i)) . b1 = b2 ./. b3
reconsider n9 = n as Element of NAT by INT_1:3;
A31: s1 . (n9 + 1) = N1 by ;
s1 . n9 = H1 by ;
then (the_series_of_quotients_of s1) . n = H1 ./. N1 by ;
hence (Del (,i)) . n = H1 ./. N1 by ; :: thesis: verum
end;
suppose n1 = i ; :: thesis: (Del (,i)) . b1 = b2 ./. b3
then ( s1 . n = H1 & s1 . (n + 1) = N1 ) by ;
then (the_series_of_quotients_of s1) . n = H1 ./. N1 by ;
hence (Del (,i)) . n = H1 ./. N1 by ; :: thesis: verum
end;
end;
end;
suppose A32: n >= i ; :: thesis: (Del (,i)) . b1 = b2 ./. b3
reconsider n19 = n1 as Element of NAT ;
( 0 + i < 1 + i & n + 1 >= i + 1 ) by ;
then n1 >= i by XXREAL_0:2;
then A33: s1 . (n19 + 1) = N1 by ;
s1 . n19 = H1 by ;
then (the_series_of_quotients_of s1) . n1 = H1 ./. N1 by ;
hence (Del (,i)) . n = H1 ./. N1 by ; :: thesis: verum
end;
end;
end;
hence the_series_of_quotients_of s2 = Del (,i) by A10, A2, A3, A9, A16, A18, A19, Def33; :: thesis: verum
end;
end;