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:
per cases ( s1 is empty or not s1 is empty ) ;
suppose A3: s1 is empty ; :: thesis:
now :: thesis: s2 is empty
now :: thesis: ex x being set st
( 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 ; :: thesis: verum
end;
then A4: s2 is_finer_than s1 ;
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: verum
end;
suppose A6: not s1 is empty ; :: thesis:
defpred S1[ 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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds
ex p being Permutation of () 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
assume A8: s2 is empty ; :: thesis: contradiction
now :: thesis: ex x being set st
( 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 ; :: thesis: verum
end;
then A9: s1 is_finer_than s2 ;
s1 is strictly_decreasing by A1;
hence contradiction by A2, A6, A8, A9; :: thesis: verum
end;
A10: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A11: S1[n] ; :: thesis: S1[n + 1]
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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds
S1[n + 1]
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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S1[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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S1[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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S1[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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S1[n + 1] )
(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:6;
then consider i being Nat such that
A14: i in dom and
A15: for H being GroupWithOperators of O st H = . i holds
H is trivial by ;
reconsider s199 = Del (s19,i) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;
A16: i in dom s19 by ;
A17: ( i + 1 in dom s19 & s19 . i = s19 . (i + 1) ) by ;
then reconsider s199 = s199 as CompositionSeries of G by ;
A18: the_series_of_quotients_of s199 = Del (,i) by ;
set f2 = the_series_of_quotients_of s29;
assume A19: s29 is_finer_than s2 ; :: thesis: ( ex p being Permutation of () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S1[n + 1] )
given p being Permutation of () such that A20: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: S1[n + 1]
set H1 = . i;
A21: (the_series_of_quotients_of s19) . i in rng by ;
set j = (p ") . i;
reconsider j = (p ") . i as Nat ;
set H2 = . j;
reconsider s299 = Del (s29,j) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;
rng (p ") c= dom ;
then A22: rng (p ") c= Seg () by FINSEQ_1:def 3;
A23: len = len by A20;
(p ") . i in rng (p ") by ;
then (p ") . i in Seg () by A22;
then A24: j in dom by ;
then (the_series_of_quotients_of s29) . j in rng by FUNCT_1:3;
then reconsider H1 = . i, H2 = . j as strict GroupWithOperators of O by ;
A25: H1 is trivial by A15;
H1,H2 are_isomorphic by ;
then A26: for H being GroupWithOperators of O st H = . j holds
H is trivial by ;
then A27: ( j in dom s29 & j + 1 in dom s29 ) by ;
A28: s29 . j = s29 . (j + 1) by ;
then reconsider s299 = s299 as CompositionSeries of G by ;
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 ;
the_series_of_quotients_of s299 = Del (,j) by ;
then A31: ex p being Permutation of () st the_series_of_quotients_of s199, the_series_of_quotients_of s299 are_equivalent_under p,O by ;
( s199 is_finer_than s1 & not s199 is empty ) by A1, A6, A13, A16, A17, Th97, Th99;
hence S1[n + 1] by A11, A30, A29, A31; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A32: S1[ 0 ]
proof
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 () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies ex p being Permutation of () 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 () 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 () 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 () 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 () 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 () 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 () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
given p being Permutation of () 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 () 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 ;
s19 = s1 by ;
then s29 is jordan_holder by ;
then s29 = s2 by ;
then s1 is_equivalent_with s2 by ;
hence ex p being Permutation of () st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by ; :: thesis: verum
end;
A38: for n being Nat holds S1[n] from 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 ;
A43: ex n being Nat st len s19 = (len s1) + n by ;
A44: not s29 is empty by ;
then ex p9 being Permutation of () st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p9,O by ;
then ex p being Permutation of () 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 ; :: thesis: verum
end;
end;