let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds
s2 is_finer_than s1

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds
s2 is_finer_than s1

let s1, s2 be CompositionSeries of G; :: thesis: ( ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 implies s2 is_finer_than s1 )
assume A1: ( len s1 <= 1 or len s2 <= 1 ) ; :: thesis: ( not len s1 <= len s2 or s2 is_finer_than s1 )
assume A2: len s1 <= len s2 ; :: thesis: s2 is_finer_than s1
then A3: len s1 <= 1 by ;
per cases ( len s1 = 1 or len s1 <> 1 ) ;
suppose A4: len s1 = 1 ; :: thesis: s2 is_finer_than s1
then A5: s1 = <*(s1 . 1)*> by FINSEQ_1:40;
now :: thesis: ex x being set st
( x c= dom s2 & s1 = s2 * (Sgm x) )
reconsider D = Seg (len s2) as non empty set by A2, A4;
set x = {1};
take x = {1}; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )
set f = s2;
set p = <*1*>;
( dom s2 = Seg (len s2) & rng s2 c= the_stable_subgroups_of G ) by FINSEQ_1:def 3;
then reconsider f = s2 as Function of D, by FUNCT_2:2;
A6: 1 in Seg (len s2) by A2, A4;
then 1 in dom s2 by FINSEQ_1:def 3;
hence x c= dom s2 by ZFMISC_1:31; :: thesis: s1 = s2 * (Sgm x)
{1} c= D by ;
then rng <*1*> c= D by FINSEQ_1:38;
then reconsider p = <*1*> as FinSequence of D by FINSEQ_1:def 4;
( Sgm x = p & f * p = <*(f . 1)*> ) by ;
then s2 * (Sgm x) = <*()*> by Def28;
hence s1 = s2 * (Sgm x) by ; :: thesis: verum
end;
hence s2 is_finer_than s1 ; :: thesis: verum
end;
suppose len s1 <> 1 ; :: thesis: s2 is_finer_than s1
then len s1 < 0 + 1 by ;
then A7: s1 = {} by NAT_1:13;
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;
hence s2 is_finer_than s1 ; :: thesis: verum
end;
end;