for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for f1 being FinSequence
for i being Nat st f1 = the_series_of_quotients_of s1 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) holds
( Del (s1,i) is CompositionSeries of G & ( for s2 being CompositionSeries of G st s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del (f1,i) ) )