let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( s2 = Del (s1,i) implies the_series_of_quotients_of s2 = Del (f1,i) )
assume s2 = Del (s1,i) ; :: thesis: the_series_of_quotients_of s2 = Del (f1,i)
hence the_series_of_quotients_of s2 = Del (f1,i) by A1, A5, A4, Th104; :: thesis: verum