:: deftheorem defines TwoValued FINSEQ_6:def 6 :
for f being FinSequence holds
( f is TwoValued iff card (rng f) = 2 );