let O be set ; 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; 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; ( 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
; ( 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
; 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; verum