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

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

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

now

assume A4: not s2 is empty ; :: thesis: contradiction
A5: s2 is strictly_decreasing by A2, Def34;

now

set x = {} ;
take x = {} ; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )
thus x c= dom s2 by XBOOLE_1:2; :: thesis: s1 = s2 * (Sgm x)
thus s1 = s2 * (Sgm x) by A3, FINSEQ_3:49; :: thesis: verum

end;

then s2 is_finer_than s1 by Def32;
hence contradiction by A1, A3, A4, A5, Def34; :: thesis: verum

end;

hence s1 is_equivalent_with s2 by A3, Th107; :: thesis: verum

end;

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

A7: now

assume A8: s2 is empty ; :: thesis: contradiction
A9: s1 is strictly_decreasing by A1, Def34;

now

set x = {} ;
take x = {} ; :: thesis: ( x c= dom s1 & s2 = s1 * (Sgm x) )
thus x c= dom s1 by XBOOLE_1:2; :: thesis: s2 = s1 * (Sgm x)
thus s2 = s1 * (Sgm x) by A8, FINSEQ_3:49; :: thesis: verum

end;

then s1 is_finer_than s2 by Def32;
hence contradiction by A2, A6, A8, A9, Def34; :: thesis: verum

end;

consider s1', s2' being CompositionSeries of G such that
A10: ( s1' is_finer_than s1 & s2' is_finer_than s2 & s1' is_equivalent_with s2' ) by Th118;
A11: ( not s1' is empty & not s2' is empty ) by A6, A7, A10, Th97;
then A12: 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 A10, Th108;
defpred S₁[ Nat] means for s1', s2' being CompositionSeries of G st not s1' is empty & not s2' is empty & len s1' = (len s1) + $1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 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;
A13: S₁[ 0 ]

proof

let s1', s2' be CompositionSeries of G; :: thesis: ( not s1' is empty & not s2' is empty & len s1' = (len s1) + 0 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 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 A14: ( not s1' is empty & not s2' is empty ) ; :: thesis: ( not len s1' = (len s1) + 0 or not s1' is_finer_than s1 or not s2' is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s1')) holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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 A15: ( len s1' = (len s1) + 0 & s1' is_finer_than s1 ) ; :: thesis: ( not s2' is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s1')) holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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 A16: s2' is_finer_than s2 ; :: thesis: ( for p being Permutation of (dom (the_series_of_quotients_of s1')) holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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 s1')) such that A17: the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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
A18: s1' is_equivalent_with s2' by A14, A17, Th108;
s1' = s1 by A15, Th96;
then s2' is jordan_holder by A1, A18, Th115;
then s2' = s2 by A2, A16, Th98;
then s1 is_equivalent_with s2 by A15, A18, 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;

A19: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A20: S₁[n] ; :: thesis: S₁[n + 1]

now

let s1', s2' be CompositionSeries of G; :: thesis: ( not s1' is empty & not s2' is empty & len s1' = ((len s1) + n) + 1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume ( not s1' is empty & not s2' is empty ) ; :: thesis: ( len s1' = ((len s1) + n) + 1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume A21: len s1' = ((len s1) + n) + 1 ; :: thesis: ( s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume A22: s1' is_finer_than s1 ; :: thesis: ( s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume A23: s2' is_finer_than s2 ; :: 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 implies S₁[n + 1] )
set f1 = the_series_of_quotients_of s1';
set f2 = the_series_of_quotients_of s2';
given p being Permutation of (dom (the_series_of_quotients_of s1')) such that A24: the_series_of_quotients_of s1', the_series_of_quotients_of s2' are_equivalent_under p,O ; :: thesis: S₁[n + 1]
A25: len (the_series_of_quotients_of s1') = len (the_series_of_quotients_of s2') by A24, Def37;
(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:8;
then consider i being Nat such that
A26: ( i in dom (the_series_of_quotients_of s1') & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1') . i holds
H is trivial ) ) by A1, A21, A22, Th109;
A27: ( i in dom s1' & i + 1 in dom s1' & s1' . i = s1' . (i + 1) ) by A26, Th103;
set j = (p " ) . i;
rng (p " ) c= dom (the_series_of_quotients_of s1') ;
then A28: rng (p " ) c= Seg (len (the_series_of_quotients_of s1')) by FINSEQ_1:def 3;
(p " ) . i in rng (p " ) by A26, FUNCT_2:6;
then A29: (p " ) . i in Seg (len (the_series_of_quotients_of s1')) by A28;
reconsider j = (p " ) . i as Nat ;
A30: j in dom (the_series_of_quotients_of s2') by A25, A29, FINSEQ_1:def 3;
set H1 = (the_series_of_quotients_of s1') . i;
set H2 = (the_series_of_quotients_of s2') . j;
A31: (the_series_of_quotients_of s1') . i in rng (the_series_of_quotients_of s1') by A26, FUNCT_1:12;
(the_series_of_quotients_of s2') . j in rng (the_series_of_quotients_of s2') by A30, FUNCT_1:12;
then reconsider H1 = (the_series_of_quotients_of s1') . i, H2 = (the_series_of_quotients_of s2') . j as strict GroupWithOperators of O by A31, Th102;
A32: H1 is trivial by A26;
H1,H2 are_isomorphic by A24, A26, Def37;
then for H being GroupWithOperators of O st H = (the_series_of_quotients_of s2') . j holds
H is trivial by A32, Th58;
then A33: ( j in dom s2' & j + 1 in dom s2' & s2' . j = s2' . (j + 1) ) by A30, Th103;
reconsider s1'' = Del s1',i as FinSequence of the_stable_subgroups_of G by FINSEQ_3:114;
reconsider s1'' = s1'' as CompositionSeries of G by A27, Th94;
reconsider s2'' = Del s2',j as FinSequence of the_stable_subgroups_of G by FINSEQ_3:114;
reconsider s2'' = s2'' as CompositionSeries of G by A33, Th94;
A34: len s1'' = (len s1) + n by A21, A27, FINSEQ_3:118;
A35: s1'' is_finer_than s1 by A1, A22, A27, Th99;
A36: s2'' is_finer_than s2 by A2, A23, A33, Th99;
A37: the_series_of_quotients_of s1'' = Del (the_series_of_quotients_of s1'),i by A27, Th104;
A38: the_series_of_quotients_of s2'' = Del (the_series_of_quotients_of s2'),j by A33, Th104;
A39: ( not s1'' is empty & not s2'' is empty ) by A1, A2, A6, A7, A22, A23, A27, A33, Th97, Th99;
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 A24, A26, A37, A38, Th106;
hence S₁[n + 1] by A20, A34, A35, A36, A39; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A40: for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A19);
ex n being Nat st len s1' = (len s1) + n by A10, Th95;
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 A10, A11, A12, A40;
hence s1 is_equivalent_with s2 by A6, A7, Th108; :: thesis: verum

end;

end;