let p be FinSequence; :: thesis: ( p is TwoValued iff ( len p > 1 & ex x, y being set st
( x <> y & rng p = {x,y} ) ) )

hereby :: thesis: ( len p > 1 & ex x, y being set st
( x <> y & rng p = {x,y} ) implies p is TwoValued )

assume p is TwoValued ; :: thesis: ( len p > 1 & ex x, y being set st
( x <> y & rng p = {x,y} ) )
then card (rng p) = 2 by Def3;
then consider x, y being set such that
A1: ( x <> y & rng p = {x,y} ) by CARD_2:79;
thus len p > 1 :: thesis: ex x, y being set st
( x <> y & rng p = {x,y} )

proof

set l = len p;
assume A2: len p <= 1 ; :: thesis: contradiction

per cases ( len p = 0 or len p = 1 ) by A2, NAT_1:26;

suppose len p = 0 ; :: thesis: contradiction

then p = {} ;
hence contradiction by A1; :: thesis: verum

end;

suppose A3: len p = 1 ; :: thesis: contradiction

then 1 in dom p by FINSEQ_3:27;
then consider z being set such that
A4: [1,z] in p by RELAT_1:def 4;
z = p . 1 by A4, FUNCT_1:8;
then p = <*z*> by A3, FINSEQ_1:57;
then rng p = {z} by FINSEQ_1:56;
then ( z = x & z = y ) by A1, ZFMISC_1:8;
hence contradiction by A1; :: thesis: verum

end;

end;

end;

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

end;

assume len p > 1 ; :: thesis: ( for x, y being set holds
( not x <> y or not rng p = {x,y} ) or p is TwoValued )
given x, y being set such that A5: ( x <> y & rng p = {x,y} ) ; :: thesis: p is TwoValued
card (rng p) = 2 by A5, CARD_2:76;
hence p is TwoValued by Def3; :: thesis: verum