theorem Th6: :: BALLOT_1:6

for f being FinSequence
for x, y being object st rng f c= {x,y} & x <> y holds
(card (f " {x})) + (card (f " {y})) = len f