let X, Y be set ; :: thesis: for n being Nat st X <> Y & n > 1 holds

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

let n be Nat; :: thesis: ( X <> Y & n > 1 implies ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X ) )

deffunc H_{1}( Nat, Nat) -> Element of omega = 3 -' $2;

assume that

A1: X <> Y and

A2: n > 1 ; :: thesis: ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

set p = <*X,Y*>;

A3: <*X,Y*> . 1 = X by FINSEQ_1:44;

A4: 3 -' 2 = (1 + 2) - 2 by XREAL_0:def 2

.= 1 ;

A5: <*X,Y*> . 2 = Y by FINSEQ_1:44;

consider f1 being sequence of NAT such that

A6: ( f1 . 0 = 2 & ( for n being Nat holds f1 . (n + 1) = H_{1}(n,f1 . n) ) )
from NAT_1:sch 12();

defpred S_{1}[ Nat] means ( ( f1 . $1 = 1 or f1 . $1 = 2 ) & f1 . $1 <> f1 . ($1 + 1) );

A7: 3 -' 1 = (2 + 1) - 1 by XREAL_0:def 2

.= 2 ;

A8: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by A6, A4;

A11: for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A10, A8);

deffunc H_{2}( Nat) -> set = <*X,Y*> . (f1 . $1);

consider p1 being FinSequence such that

A12: ( len p1 = n & ( for k being Nat st k in dom p1 holds

p1 . k = H_{2}(k) ) )
from FINSEQ_1:sch 2();

A13: f1 . (0 + 1) = 1 by A6, A4;

then A14: f1 . (1 + 1) = 2 by A6, A7;

then reconsider p1 = p1 as TwoValued FinSequence by A1, A2, A12, Th19;

take p1 ; :: thesis: ( rng p1 = {X,Y} & len p1 = n & p1 . 1 = X )

thus rng p1 = {X,Y} by A15, FUNCT_1:def 3; :: thesis: ( len p1 = n & p1 . 1 = X )

thus len p1 = n by A12; :: thesis: p1 . 1 = X

1 in dom p1 by A2, A12, FINSEQ_3:25;

hence p1 . 1 = X by A3, A13, A12; :: thesis: verum

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

let n be Nat; :: thesis: ( X <> Y & n > 1 implies ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X ) )

deffunc H

assume that

A1: X <> Y and

A2: n > 1 ; :: thesis: ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

set p = <*X,Y*>;

A3: <*X,Y*> . 1 = X by FINSEQ_1:44;

A4: 3 -' 2 = (1 + 2) - 2 by XREAL_0:def 2

.= 1 ;

A5: <*X,Y*> . 2 = Y by FINSEQ_1:44;

consider f1 being sequence of NAT such that

A6: ( f1 . 0 = 2 & ( for n being Nat holds f1 . (n + 1) = H

defpred S

A7: 3 -' 1 = (2 + 1) - 1 by XREAL_0:def 2

.= 2 ;

A8: for i being Nat st S

S

proof

A10:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume that

A9: ( f1 . i = 1 or f1 . i = 2 ) and

f1 . i <> f1 . (i + 1) ; :: thesis: S_{1}[i + 1]

thus ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) by A6, A4, A7, A9; :: thesis: f1 . (i + 1) <> f1 . ((i + 1) + 1)

hence f1 . (i + 1) <> f1 . ((i + 1) + 1) by A6, A4, A7; :: thesis: verum

end;assume that

A9: ( f1 . i = 1 or f1 . i = 2 ) and

f1 . i <> f1 . (i + 1) ; :: thesis: S

thus ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) by A6, A4, A7, A9; :: thesis: f1 . (i + 1) <> f1 . ((i + 1) + 1)

hence f1 . (i + 1) <> f1 . ((i + 1) + 1) by A6, A4, A7; :: thesis: verum

A11: for i being Nat holds S

deffunc H

consider p1 being FinSequence such that

A12: ( len p1 = n & ( for k being Nat st k in dom p1 holds

p1 . k = H

A13: f1 . (0 + 1) = 1 by A6, A4;

then A14: f1 . (1 + 1) = 2 by A6, A7;

A15: now :: thesis: for y being object holds

( ( y in {X,Y} implies ex x being object st

( x in dom p1 & y = p1 . x ) ) & ( ex x being object st

( x in dom p1 & y = p1 . x ) implies y in {X,Y} ) )

then
rng p1 = {X,Y}
by FUNCT_1:def 3;( ( y in {X,Y} implies ex x being object st

( x in dom p1 & y = p1 . x ) ) & ( ex x being object st

( x in dom p1 & y = p1 . x ) implies y in {X,Y} ) )

let y be object ; :: thesis: ( ( y in {X,Y} implies ex x being object st

( x in dom p1 & y = p1 . x ) ) & ( ex x being object st

( x in dom p1 & y = p1 . x ) implies y in {X,Y} ) )

A21: y = p1 . x ; :: thesis: y in {X,Y}

x in Seg (len p1) by A20, FINSEQ_1:def 3;

then consider x9 being Nat such that

A22: x9 = x and

A23: 1 <= x9 and

A24: x9 <= len p1 ;

x9 in dom p1 by A23, A24, FINSEQ_3:25;

then A25: p1 . x9 = <*X,Y*> . (f1 . x9) by A12;

( f1 . x9 = 1 or f1 . x9 = 2 ) by A11;

hence y in {X,Y} by A3, A5, A21, A22, A25, TARSKI:def 2; :: thesis: verum

end;( x in dom p1 & y = p1 . x ) ) & ( ex x being object st

( x in dom p1 & y = p1 . x ) implies y in {X,Y} ) )

hereby :: thesis: ( ex x being object st

( x in dom p1 & y = p1 . x ) implies y in {X,Y} )

given x being object such that A20:
x in dom p1
and ( x in dom p1 & y = p1 . x ) implies y in {X,Y} )

assume
y in {X,Y}
; :: thesis: ex x being object st

( x in dom p1 & y = p1 . x )

then A16: ( y = X or y = Y ) by TARSKI:def 2;

1 in dom p1 by A2, A12, FINSEQ_3:25;

then A17: p1 . 1 = X by A3, A13, A12;

A18: 1 in dom p1 by A2, A12, FINSEQ_3:25;

1 + 1 <= n by A2, NAT_1:13;

then A19: 2 in dom p1 by A12, FINSEQ_3:25;

then p1 . 2 = Y by A5, A14, A12;

hence ex x being object st

( x in dom p1 & y = p1 . x ) by A16, A19, A17, A18; :: thesis: verum

end;( x in dom p1 & y = p1 . x )

then A16: ( y = X or y = Y ) by TARSKI:def 2;

1 in dom p1 by A2, A12, FINSEQ_3:25;

then A17: p1 . 1 = X by A3, A13, A12;

A18: 1 in dom p1 by A2, A12, FINSEQ_3:25;

1 + 1 <= n by A2, NAT_1:13;

then A19: 2 in dom p1 by A12, FINSEQ_3:25;

then p1 . 2 = Y by A5, A14, A12;

hence ex x being object st

( x in dom p1 & y = p1 . x ) by A16, A19, A17, A18; :: thesis: verum

A21: y = p1 . x ; :: thesis: y in {X,Y}

x in Seg (len p1) by A20, FINSEQ_1:def 3;

then consider x9 being Nat such that

A22: x9 = x and

A23: 1 <= x9 and

A24: x9 <= len p1 ;

x9 in dom p1 by A23, A24, FINSEQ_3:25;

then A25: p1 . x9 = <*X,Y*> . (f1 . x9) by A12;

( f1 . x9 = 1 or f1 . x9 = 2 ) by A11;

hence y in {X,Y} by A3, A5, A21, A22, A25, TARSKI:def 2; :: thesis: verum

then reconsider p1 = p1 as TwoValued FinSequence by A1, A2, A12, Th19;

now :: thesis: for i being Nat st 1 <= i & i + 1 <= len p1 holds

p1 . i <> p1 . (i + 1)

then reconsider p1 = p1 as TwoValued Alternating FinSequence by Def4;p1 . i <> p1 . (i + 1)

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len p1 implies p1 . i <> p1 . (i + 1) )

assume that

A26: 1 <= i and

A27: i + 1 <= len p1 ; :: thesis: p1 . i <> p1 . (i + 1)

1 <= i + 1 by A26, NAT_1:13;

then i + 1 in dom p1 by A27, FINSEQ_3:25;

then A28: p1 . (i + 1) = <*X,Y*> . (f1 . (i + 1)) by A12;

A29: ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) by A11;

i <= n by A12, A27, NAT_1:13;

then i in dom p1 by A12, A26, FINSEQ_3:25;

then p1 . i = <*X,Y*> . (f1 . i) by A12;

hence p1 . i <> p1 . (i + 1) by A1, A3, A5, A11, A28, A29; :: thesis: verum

end;assume that

A26: 1 <= i and

A27: i + 1 <= len p1 ; :: thesis: p1 . i <> p1 . (i + 1)

1 <= i + 1 by A26, NAT_1:13;

then i + 1 in dom p1 by A27, FINSEQ_3:25;

then A28: p1 . (i + 1) = <*X,Y*> . (f1 . (i + 1)) by A12;

A29: ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) by A11;

i <= n by A12, A27, NAT_1:13;

then i in dom p1 by A12, A26, FINSEQ_3:25;

then p1 . i = <*X,Y*> . (f1 . i) by A12;

hence p1 . i <> p1 . (i + 1) by A1, A3, A5, A11, A28, A29; :: thesis: verum

take p1 ; :: thesis: ( rng p1 = {X,Y} & len p1 = n & p1 . 1 = X )

thus rng p1 = {X,Y} by A15, FUNCT_1:def 3; :: thesis: ( len p1 = n & p1 . 1 = X )

thus len p1 = n by A12; :: thesis: p1 . 1 = X

1 in dom p1 by A2, A12, FINSEQ_3:25;

hence p1 . 1 = X by A3, A13, A12; :: thesis: verum