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 A1, XXREAL_0:2;

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,(the_stable_subgroups_of G) 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 A6, ZFMISC_1:31;
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 FINSEQ_2:35, FINSEQ_3:44;
then s2 * (Sgm x) = <*((Omega). G)*> by Def28;
hence s1 = s2 * (Sgm x) by A5, Def28; :: 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 A3, XXREAL_0:1;
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 A7, FINSEQ_3:43; :: thesis: verum

end;

hence s2 is_finer_than s1 ; :: thesis: verum

end;

end;