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;

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;

end;

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;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

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;

end;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

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: verumfor 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_{3} = b_{4} ./. b_{5} )

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_{3} = b_{4} ./. b_{5}

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_{2} = b_{3} ./. b_{4}

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_{1} = b_{2} ./. b_{3} )

assume A24: H1 = s2 . n ; :: thesis: ( N1 = s2 . (n + 1) implies (Del ((the_series_of_quotients_of s1),i)) . b_{1} = b_{2} ./. b_{3} )

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_{1} = b_{2} ./. b_{3}

end;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

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

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

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

assume A24: H1 = s2 . n ; :: thesis: ( N1 = s2 . (n + 1) implies (Del ((the_series_of_quotients_of s1),i)) . 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

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

end;

suppose A28:
n < i
; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b_{1} = b_{2} ./. b_{3}

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

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

end;

suppose A30:
n1 < i
; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b_{1} = b_{2} ./. b_{3}

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;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

suppose
n1 = i
; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b_{1} = b_{2} ./. b_{3}

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;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

suppose A32:
n >= i
; :: thesis: (Del ((the_series_of_quotients_of s1),i)) . b_{1} = b_{2} ./. b_{3}

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;( 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