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 ;
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 ;
then p = <*z*> by ;
then A6: rng p = {z} by FINSEQ_1:39;
then z = x by ;
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 ;
hence p is TwoValued ; :: thesis: verum