let O be 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) ) )
let G be 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) ) )
let s1 be 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) ) )
let f1 be 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) ) )
let i be Nat; ( 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 ) implies ( 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) ) ) )
assume A1:
f1 = the_series_of_quotients_of s1
; ( not i in dom f1 or ex H being GroupWithOperators of O st
( H = f1 . i & not H is trivial ) or ( 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) ) ) )
assume A2:
i in dom f1
; ( ex H being GroupWithOperators of O st
( H = f1 . i & not H is trivial ) or ( 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) ) ) )
assume A3:
for H being GroupWithOperators of O st H = f1 . i holds
H is trivial
; ( 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) ) )
then A4:
s1 . i = s1 . (i + 1)
by A1, A2, Th103;
A5:
( i in dom s1 & i + 1 in dom s1 )
by A1, A2, A3, Th103;
hence
Del (s1,i) is CompositionSeries of G
by A4, Th94, FINSEQ_3:105; for s2 being CompositionSeries of G st s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del (f1,i)
let s2 be CompositionSeries of G; ( s2 = Del (s1,i) implies the_series_of_quotients_of s2 = Del (f1,i) )
assume
s2 = Del (s1,i)
; the_series_of_quotients_of s2 = Del (f1,i)
hence
the_series_of_quotients_of s2 = Del (f1,i)
by A1, A5, A4, Th104; verum