let f be FinSequence; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: (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}

proof

assume f " {A} meets f " {B} ; :: thesis: contradiction
then consider x being object such that
A5: x in f " {A} and
A6: x in f " {B} by XBOOLE_0:3;
A7: f . x in {A} by A5, FUNCT_1:def 7;
A8: f . x in {B} by A6, FUNCT_1:def 7;
f . x = A by A7, TARSKI:def 1;
hence contradiction by A8, TARSKI:def 1, A3; :: thesis: verum

end;

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 ;
:: thesis: verum