let f be FinSequence; for x, y being object st rng f c= {x,y} & x <> y holds
(card (f " {x})) + (card (f " {y})) = len f
let A, B be object ; ( rng f c= {A,B} & A <> B implies (card (f " {A})) + (card (f " {B})) = len f )
A1:
{A} \/ {B} = {A,B}
by ENUMSET1:1;
assume that
A2:
rng f c= {A,B}
and
A3:
A <> B
; (card (f " {A})) + (card (f " {B})) = len f
f " (rng f) c= f " {A,B}
by A2, RELAT_1:143;
then A4: dom f =
f " {A,B}
by RELAT_1:132, RELAT_1:134
.=
(f " {A}) \/ (f " {B})
by RELAT_1:140, A1
;
f " {A} misses f " {B}
hence (card (f " {A})) + (card (f " {B})) =
card (dom f)
by A4, CARD_2:40
.=
card (Seg (len f))
by FINSEQ_1:def 3
.=
len f
by FINSEQ_1:57
;
verum