let p be FinSequence; :: thesis:

hereby :: thesis:

assume p is TwoValued ; :: thesis:
then card (rng p) = 2 ;
then consider x, y being object such that
A1: x <> y and
A2: rng p = {x,y} by CARD_2:60;
thus len p > 1 :: thesis:

set l = len p;
assume A3: len p <= 1 ; :: thesis:

per cases by A3, NAT_1:25;

suppose len p = 0 ; :: thesis:

then p = {} ;
hence contradiction by A2; :: thesis:

end;

suppose A4: len p = 1 ; :: thesis:

then 1 in dom p by FINSEQ_3:25;
then consider z being object such that
A5: [1,z] in p by XTUPLE_0:def 12;
z = p . 1 by A5, FUNCT_1:1;
then p = <*z*> by A4, FINSEQ_1:40;
then A6: rng p = {z} by FINSEQ_1:39;
then z = x by A2, ZFMISC_1:4;
hence contradiction by A1, A2, A6, ZFMISC_1:4; :: thesis:

end;

end;

end;

thus ex x, y being object st
( x <> y & rng p = {x,y} ) by A1, A2; :: thesis:

end;

assume len p > 1 ; :: thesis:
given x, y being object such that A7: x <> y and
A8: rng p = {x,y} ; :: thesis:
card (rng p) = 2 by A7, A8, CARD_2:57;
hence p is TwoValued ; :: thesis: