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

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