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

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

assume p is TwoValued ; :: thesis: ( len p > 1 & ex x, y being object st
( x <> y & rng p = {x,y} ) )
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: ex x, y being object st
( x <> y & rng p = {x,y} )

proof

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

per cases ( len p = 0 or len p = 1 ) by A3, NAT_1:25;

suppose len p = 0 ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

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

end;

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