let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds
ex n being Nat st len s1 = (len s2) + n

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds
ex n being Nat st len s1 = (len s2) + n

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 implies ex n being Nat st len s1 = (len s2) + n )
set n = (len s1) - (len s2);
assume s1 is_finer_than s2 ; :: thesis: ex n being Nat st len s1 = (len s2) + n
then consider x being set such that
A1: x c= dom s1 and
A2: s2 = s1 * (Sgm x) ;
A3: x c= Seg (len s1) by ;
reconsider x = x as finite set by A1;
now :: thesis: for y1 being object st y1 in dom s2 holds
y1 in dom s1
let y1 be object ; :: thesis: ( y1 in dom s2 implies y1 in dom s1 )
assume y1 in dom s2 ; :: thesis: y1 in dom s1
then y1 in dom (Sgm x) by ;
then A4: y1 in Seg (card x) by ;
card x <= card (dom s1) by ;
then Seg (card x) c= Seg (card (dom s1)) by FINSEQ_1:5;
then y1 in Seg (card (dom s1)) by A4;
then y1 in Seg (card (Seg (len s1))) by FINSEQ_1:def 3;
then y1 in Seg (len s1) by FINSEQ_1:57;
hence y1 in dom s1 by FINSEQ_1:def 3; :: thesis: verum
end;
then dom s2 c= dom s1 ;
then Seg (len s2) c= dom s1 by FINSEQ_1:def 3;
then Seg (len s2) c= Seg (len s1) by FINSEQ_1:def 3;
then len s2 <= len s1 by FINSEQ_1:5;
then (len s2) - (len s2) <= (len s1) - (len s2) by XREAL_1:9;
then (len s1) - (len s2) in NAT by INT_1:3;
then reconsider n = (len s1) - (len s2) as Nat ;
take n ; :: thesis: len s1 = (len s2) + n
thus len s1 = (len s2) + n ; :: thesis: verum