let O be set ; :: thesis: for G being GroupWithOperators of O

for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds

s1 is_equivalent_with s2

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds

s1 is_equivalent_with s2

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is jordan_holder & s2 is jordan_holder implies s1 is_equivalent_with s2 )

assume A1: s1 is jordan_holder ; :: thesis: ( not s2 is jordan_holder or s1 is_equivalent_with s2 )

assume A2: s2 is jordan_holder ; :: thesis: s1 is_equivalent_with s2

for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds

s1 is_equivalent_with s2

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds

s1 is_equivalent_with s2

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is jordan_holder & s2 is jordan_holder implies s1 is_equivalent_with s2 )

assume A1: s1 is jordan_holder ; :: thesis: ( not s2 is jordan_holder or s1 is_equivalent_with s2 )

assume A2: s2 is jordan_holder ; :: thesis: s1 is_equivalent_with s2

per cases
( s1 is empty or not s1 is empty )
;

end;

suppose A3:
s1 is empty
; :: thesis: s1 is_equivalent_with s2

end;

now :: thesis: s2 is empty

assume A5: not s2 is empty ; :: thesis: contradiction

s2 is strictly_decreasing by A2;

hence contradiction by A1, A3, A5, A4; :: thesis: verum

end;

hence
s1 is_equivalent_with s2
by A3; :: thesis: verumnow :: thesis: ex x being set st

( x c= dom s2 & s1 = s2 * (Sgm x) )

then A4:
s2 is_finer_than s1
;( x c= dom s2 & s1 = s2 * (Sgm x) )

set x = {} ;

take x = {} ; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )

thus x c= dom s2 ; :: thesis: s1 = s2 * (Sgm x)

thus s1 = s2 * (Sgm x) by A3, FINSEQ_3:43; :: thesis: verum

end;take x = {} ; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )

thus x c= dom s2 ; :: thesis: s1 = s2 * (Sgm x)

thus s1 = s2 * (Sgm x) by A3, FINSEQ_3:43; :: thesis: verum

assume A5: not s2 is empty ; :: thesis: contradiction

s2 is strictly_decreasing by A2;

hence contradiction by A1, A3, A5, A4; :: thesis: verum

suppose A6:
not s1 is empty
; :: thesis: s1 is_equivalent_with s2

defpred S_{1}[ Nat] means for s19, s29 being CompositionSeries of G st not s19 is empty & not s29 is empty & len s19 = (len s1) + $1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds

ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O;

_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A32, A10);

consider s19, s29 being CompositionSeries of G such that

A39: s19 is_finer_than s1 and

A40: s29 is_finer_than s2 and

A41: s19 is_equivalent_with s29 by Th118;

A42: not s19 is empty by A6, A39;

A43: ex n being Nat st len s19 = (len s1) + n by A39, Th95;

A44: not s29 is empty by A7, A40;

then ex p9 being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p9,O by A41, A42, Th108;

then ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A39, A40, A42, A44, A38, A43;

hence s1 is_equivalent_with s2 by A6, A7, Th108; :: thesis: verum

end;ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O;

A7: now :: thesis: not s2 is empty

A10:
for n being Nat st Sassume A8:
s2 is empty
; :: thesis: contradiction

s1 is strictly_decreasing by A1;

hence contradiction by A2, A6, A8, A9; :: thesis: verum

end;now :: thesis: ex x being set st

( x c= dom s1 & s2 = s1 * (Sgm x) )

then A9:
s1 is_finer_than s2
;( x c= dom s1 & s2 = s1 * (Sgm x) )

set x = {} ;

take x = {} ; :: thesis: ( x c= dom s1 & s2 = s1 * (Sgm x) )

thus x c= dom s1 ; :: thesis: s2 = s1 * (Sgm x)

thus s2 = s1 * (Sgm x) by A8, FINSEQ_3:43; :: thesis: verum

end;take x = {} ; :: thesis: ( x c= dom s1 & s2 = s1 * (Sgm x) )

thus x c= dom s1 ; :: thesis: s2 = s1 * (Sgm x)

thus s2 = s1 * (Sgm x) by A8, FINSEQ_3:43; :: thesis: verum

s1 is strictly_decreasing by A1;

hence contradiction by A2, A6, A8, A9; :: thesis: verum

S

proof

A32:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A11: S_{1}[n]
; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
; :: thesis: verum

end;assume A11: S

now :: thesis: for s19, s29 being CompositionSeries of G st not s19 is empty & not s29 is empty & len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds

S_{1}[n + 1]

hence
SS

let s19, s29 be CompositionSeries of G; :: thesis: ( not s19 is empty & not s29 is empty & len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S_{1}[n + 1] )

assume that

not s19 is empty and

not s29 is empty ; :: thesis: ( len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S_{1}[n + 1] )

assume A12: len s19 = ((len s1) + n) + 1 ; :: thesis: ( s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S_{1}[n + 1] )

set f1 = the_series_of_quotients_of s19;

assume A13: s19 is_finer_than s1 ; :: thesis: ( s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S_{1}[n + 1] )

(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:6;

then consider i being Nat such that

A14: i in dom (the_series_of_quotients_of s19) and

A15: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s19) . i holds

H is trivial by A1, A12, A13, Th109;

reconsider s199 = Del (s19,i) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;

A16: i in dom s19 by A14, A15, Th103;

A17: ( i + 1 in dom s19 & s19 . i = s19 . (i + 1) ) by A14, A15, Th103;

then reconsider s199 = s199 as CompositionSeries of G by A16, Th94;

A18: the_series_of_quotients_of s199 = Del ((the_series_of_quotients_of s19),i) by A16, A17, Th104;

set f2 = the_series_of_quotients_of s29;

assume A19: s29 is_finer_than s2 ; :: thesis: ( ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S_{1}[n + 1] )

given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A20: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: S_{1}[n + 1]

set H1 = (the_series_of_quotients_of s19) . i;

A21: (the_series_of_quotients_of s19) . i in rng (the_series_of_quotients_of s19) by A14, FUNCT_1:3;

set j = (p ") . i;

reconsider j = (p ") . i as Nat ;

set H2 = (the_series_of_quotients_of s29) . j;

reconsider s299 = Del (s29,j) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;

rng (p ") c= dom (the_series_of_quotients_of s19) ;

then A22: rng (p ") c= Seg (len (the_series_of_quotients_of s19)) by FINSEQ_1:def 3;

A23: len (the_series_of_quotients_of s19) = len (the_series_of_quotients_of s29) by A20;

(p ") . i in rng (p ") by A14, FUNCT_2:4;

then (p ") . i in Seg (len (the_series_of_quotients_of s19)) by A22;

then A24: j in dom (the_series_of_quotients_of s29) by A23, FINSEQ_1:def 3;

then (the_series_of_quotients_of s29) . j in rng (the_series_of_quotients_of s29) by FUNCT_1:3;

then reconsider H1 = (the_series_of_quotients_of s19) . i, H2 = (the_series_of_quotients_of s29) . j as strict GroupWithOperators of O by A21, Th102;

A25: H1 is trivial by A15;

H1,H2 are_isomorphic by A20, A14;

then A26: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s29) . j holds

H is trivial by A25, Th58;

then A27: ( j in dom s29 & j + 1 in dom s29 ) by A24, Th103;

A28: s29 . j = s29 . (j + 1) by A24, A26, Th103;

then reconsider s299 = s299 as CompositionSeries of G by A27, Th94;

A29: ( s299 is_finer_than s2 & not s299 is empty ) by A2, A7, A19, A27, A28, Th97, Th99;

A30: len s199 = (len s1) + n by A12, A16, FINSEQ_3:109;

the_series_of_quotients_of s299 = Del ((the_series_of_quotients_of s29),j) by A27, A28, Th104;

then A31: ex p being Permutation of (dom (the_series_of_quotients_of s199)) st the_series_of_quotients_of s199, the_series_of_quotients_of s299 are_equivalent_under p,O by A20, A14, A18, Th106;

( s199 is_finer_than s1 & not s199 is empty ) by A1, A6, A13, A16, A17, Th97, Th99;

hence S_{1}[n + 1]
by A11, A30, A29, A31; :: thesis: verum

end;assume that

not s19 is empty and

not s29 is empty ; :: thesis: ( len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S

assume A12: len s19 = ((len s1) + n) + 1 ; :: thesis: ( s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S

set f1 = the_series_of_quotients_of s19;

assume A13: s19 is_finer_than s1 ; :: thesis: ( s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S

(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:6;

then consider i being Nat such that

A14: i in dom (the_series_of_quotients_of s19) and

A15: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s19) . i holds

H is trivial by A1, A12, A13, Th109;

reconsider s199 = Del (s19,i) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;

A16: i in dom s19 by A14, A15, Th103;

A17: ( i + 1 in dom s19 & s19 . i = s19 . (i + 1) ) by A14, A15, Th103;

then reconsider s199 = s199 as CompositionSeries of G by A16, Th94;

A18: the_series_of_quotients_of s199 = Del ((the_series_of_quotients_of s19),i) by A16, A17, Th104;

set f2 = the_series_of_quotients_of s29;

assume A19: s29 is_finer_than s2 ; :: thesis: ( ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S

given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A20: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: S

set H1 = (the_series_of_quotients_of s19) . i;

A21: (the_series_of_quotients_of s19) . i in rng (the_series_of_quotients_of s19) by A14, FUNCT_1:3;

set j = (p ") . i;

reconsider j = (p ") . i as Nat ;

set H2 = (the_series_of_quotients_of s29) . j;

reconsider s299 = Del (s29,j) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;

rng (p ") c= dom (the_series_of_quotients_of s19) ;

then A22: rng (p ") c= Seg (len (the_series_of_quotients_of s19)) by FINSEQ_1:def 3;

A23: len (the_series_of_quotients_of s19) = len (the_series_of_quotients_of s29) by A20;

(p ") . i in rng (p ") by A14, FUNCT_2:4;

then (p ") . i in Seg (len (the_series_of_quotients_of s19)) by A22;

then A24: j in dom (the_series_of_quotients_of s29) by A23, FINSEQ_1:def 3;

then (the_series_of_quotients_of s29) . j in rng (the_series_of_quotients_of s29) by FUNCT_1:3;

then reconsider H1 = (the_series_of_quotients_of s19) . i, H2 = (the_series_of_quotients_of s29) . j as strict GroupWithOperators of O by A21, Th102;

A25: H1 is trivial by A15;

H1,H2 are_isomorphic by A20, A14;

then A26: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s29) . j holds

H is trivial by A25, Th58;

then A27: ( j in dom s29 & j + 1 in dom s29 ) by A24, Th103;

A28: s29 . j = s29 . (j + 1) by A24, A26, Th103;

then reconsider s299 = s299 as CompositionSeries of G by A27, Th94;

A29: ( s299 is_finer_than s2 & not s299 is empty ) by A2, A7, A19, A27, A28, Th97, Th99;

A30: len s199 = (len s1) + n by A12, A16, FINSEQ_3:109;

the_series_of_quotients_of s299 = Del ((the_series_of_quotients_of s29),j) by A27, A28, Th104;

then A31: ex p being Permutation of (dom (the_series_of_quotients_of s199)) st the_series_of_quotients_of s199, the_series_of_quotients_of s299 are_equivalent_under p,O by A20, A14, A18, Th106;

( s199 is_finer_than s1 & not s199 is empty ) by A1, A6, A13, A16, A17, Th97, Th99;

hence S

proof

A38:
for n being Nat holds S
let s19, s29 be CompositionSeries of G; :: thesis: ( not s19 is empty & not s29 is empty & len s19 = (len s1) + 0 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

assume A33: ( not s19 is empty & not s29 is empty ) ; :: thesis: ( not len s19 = (len s1) + 0 or not s19 is_finer_than s1 or not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

assume A34: ( len s19 = (len s1) + 0 & s19 is_finer_than s1 ) ; :: thesis: ( not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

assume A35: s29 is_finer_than s2 ; :: thesis: ( for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A36: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

A37: s19 is_equivalent_with s29 by A33, A36, Th108;

s19 = s1 by A34, Th96;

then s29 is jordan_holder by A1, A37, Th115;

then s29 = s2 by A2, A35;

then s1 is_equivalent_with s2 by A34, A37, Th96;

hence ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6, A7, Th108; :: thesis: verum

end;assume A33: ( not s19 is empty & not s29 is empty ) ; :: thesis: ( not len s19 = (len s1) + 0 or not s19 is_finer_than s1 or not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

assume A34: ( len s19 = (len s1) + 0 & s19 is_finer_than s1 ) ; :: thesis: ( not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

assume A35: s29 is_finer_than s2 ; :: thesis: ( for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A36: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O

A37: s19 is_equivalent_with s29 by A33, A36, Th108;

s19 = s1 by A34, Th96;

then s29 is jordan_holder by A1, A37, Th115;

then s29 = s2 by A2, A35;

then s1 is_equivalent_with s2 by A34, A37, Th96;

hence ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6, A7, Th108; :: thesis: verum

consider s19, s29 being CompositionSeries of G such that

A39: s19 is_finer_than s1 and

A40: s29 is_finer_than s2 and

A41: s19 is_equivalent_with s29 by Th118;

A42: not s19 is empty by A6, A39;

A43: ex n being Nat st len s19 = (len s1) + n by A39, Th95;

A44: not s29 is empty by A7, A40;

then ex p9 being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p9,O by A41, A42, Th108;

then ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A39, A40, A42, A44, A38, A43;

hence s1 is_equivalent_with s2 by A6, A7, Th108; :: thesis: verum