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

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

let s1, s2 be CompositionSeries of G; :: thesis: ( len s2 = len s1 & s2 is_finer_than s1 implies s1 = s2 )
reconsider X = Seg (len s2) as finite set ;
assume len s2 = len s1 ; :: thesis: ( not s2 is_finer_than s1 or s1 = s2 )
then A1: dom s1 = Seg (len s2) by FINSEQ_1:def 3
.= dom s2 by FINSEQ_1:def 3 ;
assume s2 is_finer_than s1 ; :: thesis: s1 = s2
then consider x being set such that
A2: x c= dom s2 and
A3: s1 = s2 * (Sgm x) ;
set y = X \ x;
A4: x c= Seg (len s2) by ;
then x = rng (Sgm x) by FINSEQ_1:def 13;
then A5: dom (s2 * (Sgm x)) = dom (Sgm x) by ;
reconsider x = x, y = X \ x as finite set by A2;
dom (Sgm x) = Seg (len s2) by ;
then len (Sgm x) = len s2 by FINSEQ_1:def 3;
then A6: card x = len s2 by ;
A7: X = X \/ x by
.= x \/ y by XBOOLE_1:39 ;
card (x \/ y) = (card x) + (card y) by ;
then len s2 = (card x) + (card y) by ;
then y = {} by A6;
then Sgm x = idseq (len s2) by ;
hence s1 = s2 by ; :: thesis: verum