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 A2, FINSEQ_1:def 3;

then x = rng (Sgm x) by FINSEQ_1:def 13;

then A5: dom (s2 * (Sgm x)) = dom (Sgm x) by A2, RELAT_1:27;

reconsider x = x, y = X \ x as finite set by A2;

dom (Sgm x) = Seg (len s2) by A3, A1, A5, FINSEQ_1:def 3;

then len (Sgm x) = len s2 by FINSEQ_1:def 3;

then A6: card x = len s2 by A4, FINSEQ_3:39;

A7: X = X \/ x by A4, XBOOLE_1:12

.= x \/ y by XBOOLE_1:39 ;

card (x \/ y) = (card x) + (card y) by CARD_2:40, XBOOLE_1:79;

then len s2 = (card x) + (card y) by A7, FINSEQ_1:57;

then y = {} by A6;

then Sgm x = idseq (len s2) by A7, FINSEQ_3:48;

hence s1 = s2 by A3, FINSEQ_2:54; :: thesis: verum

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 A2, FINSEQ_1:def 3;

then x = rng (Sgm x) by FINSEQ_1:def 13;

then A5: dom (s2 * (Sgm x)) = dom (Sgm x) by A2, RELAT_1:27;

reconsider x = x, y = X \ x as finite set by A2;

dom (Sgm x) = Seg (len s2) by A3, A1, A5, FINSEQ_1:def 3;

then len (Sgm x) = len s2 by FINSEQ_1:def 3;

then A6: card x = len s2 by A4, FINSEQ_3:39;

A7: X = X \/ x by A4, XBOOLE_1:12

.= x \/ y by XBOOLE_1:39 ;

card (x \/ y) = (card x) + (card y) by CARD_2:40, XBOOLE_1:79;

then len s2 = (card x) + (card y) by A7, FINSEQ_1:57;

then y = {} by A6;

then Sgm x = idseq (len s2) by A7, FINSEQ_3:48;

hence s1 = s2 by A3, FINSEQ_2:54; :: thesis: verum