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 H1( 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) = H1(n,f1 . n) ) ) from NAT_1:sch 12();
defpred S1[ 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 S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume that
A9: ( f1 . i = 1 or f1 . i = 2 ) and
f1 . i <> f1 . (i + 1) ; :: thesis: S1[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: S1[ 0 ] by A6, A4;
A11: for i being Nat holds S1[i] from NAT_1:sch 2(A10, A8);
deffunc H2( 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 = H2(k) ) ) from 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 ;
then A17: p1 . 1 = X by A3, A13, A12;
A18: 1 in dom p1 by ;
1 + 1 <= n by ;
then A19: 2 in dom p1 by ;
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 ;
then consider x9 being Nat such that
A22: x9 = x and
A23: 1 <= x9 and
A24: x9 <= len p1 ;
x9 in dom p1 by ;
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 ; :: 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 ;
then i + 1 in dom p1 by ;
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 ;
then i in dom p1 by ;
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 ; :: thesis: ( len p1 = n & p1 . 1 = X )
thus len p1 = n by A12; :: thesis: p1 . 1 = X
1 in dom p1 by ;
hence p1 . 1 = X by A3, A13, A12; :: thesis: verum