for O being set
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)