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₁( 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 ;
A4: 3 -' 2 = (1 + 2) - 2 by XREAL_0:def 2
.= 1 ;
A5: <*X,Y*> . 2 = Y ;
consider f1 being sequence of NAT such that
A6: ( f1 . 0 = 2 & ( for n being Nat holds f1 . (n + 1) = H₁(n,f1 . n) ) ) from NAT_1:sch 12();
defpred S₁[ 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₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A9: ( f1 . i = 1 or f1 . i = 2 ) and
f1 . i <> f1 . (i + 1) ; :: thesis: S₁[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;

A10: S₁[ 0 ] by A6, A4;
A11: for i being Nat holds S₁[i] from NAT_1:sch 2(A10, A8);
deffunc H₂( 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₂(k) ) ) from FINSEQ_1:sch 2();
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} ) )

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} ) )

hereby :: thesis: ( ex x being object st
( 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;

given x being object such that A20: x in dom p1 and
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 A21, A22, A25, TARSKI:def 2; :: thesis: verum

end;

then rng p1 = {X,Y} by FUNCT_1:def 3;
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)

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;

then reconsider p1 = p1 as TwoValued Alternating FinSequence by Def4;
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