let p be FinSequence; :: thesis: ( p is TwoValued iff ( len p > 1 & ex x, y being object st

( x <> y & rng p = {x,y} ) ) )

( 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

( 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
len p > 1
; :: thesis: ( for x, y being object holds ( 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} )

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

end;( 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

thus
ex x, y being object st
set l = len p;

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

end;assume A3: len p <= 1 ; :: thesis: contradiction

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

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;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

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

( 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