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 a4: x is included_in_Seg ;
then x = rng (Sgm x) by FINSEQ_1:def 14;
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