let X, Y be set ; :: thesis: for n being Element of 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 Element of NAT ; :: thesis: ( X <> Y & n > 1 implies ex a1 being TwoValued Alternating FinSequence st
( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X ) )
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 & <*X,Y*> . 2 = Y ) by FINSEQ_1:61;
deffunc H₁( Nat, Nat) -> Element of NAT = 3 -' $2;
consider f1 being Function of NAT ,NAT such that
A4: ( f1 . 0 = 2 & ( for n being Nat holds f1 . (n + 1) = H₁(n,f1 . n) ) ) from NAT_1:sch 12();
defpred S₁[ Element of NAT ] means ( ( f1 . $1 = 1 or f1 . $1 = 2 ) & f1 . $1 <> f1 . ($1 + 1) );

A5: now

thus A6: 3 -' 2 = (1 + 2) - 2 by XREAL_0:def 2
.= 1 ; :: thesis: ( 3 -' 1 = 2 & f1 . (0 + 1) = 1 & f1 . (1 + 1) = 2 )
thus A7: 3 -' 1 = (2 + 1) - 1 by XREAL_0:def 2
.= 2 ; :: thesis: ( f1 . (0 + 1) = 1 & f1 . (1 + 1) = 2 )
thus f1 . (0 + 1) = 1 by A4, A6; :: thesis: f1 . (1 + 1) = 2
hence f1 . (1 + 1) = 2 by A4, A7; :: thesis: verum

end;

then A8: S₁[ 0 ] by A4;
A9: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A10: ( ( f1 . i = 1 or f1 . i = 2 ) & f1 . i <> f1 . (i + 1) ) ; :: thesis: S₁[i + 1]
thus ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) by A4, A5, A10; :: thesis: f1 . (i + 1) <> f1 . ((i + 1) + 1)
hence f1 . (i + 1) <> f1 . ((i + 1) + 1) by A4, A5; :: thesis: verum

end;

A11: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A8, A9);
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: now

let y be set ; :: thesis: ( ( y in {X,Y} implies ex x being set st
( x in dom p1 & y = p1 . x ) ) & ( ex x being set st
( x in dom p1 & y = p1 . x ) implies y in {X,Y} ) )

hereby :: thesis: ( ex x being set st
( x in dom p1 & y = p1 . x ) implies y in {X,Y} )

assume y in {X,Y} ; :: thesis: ex x being set st
( x in dom p1 & y = p1 . x )
then A14: ( y = X or y = Y ) by TARSKI:def 2;
1 + 1 <= n by A2, NAT_1:13;
then ( 1 <= 1 & 1 <= len p1 & 1 <= 2 & 2 <= len p1 ) by A12, XXREAL_0:2;
then A15: ( 1 in dom p1 & 2 in dom p1 ) by FINSEQ_3:27;
then A16: ( p1 . 1 = X & p1 . 2 = Y ) by A3, A5, A12;
( 1 in dom p1 & 2 in dom p1 ) by A15;
hence ex x being set st
( x in dom p1 & y = p1 . x ) by A14, A16; :: thesis: verum

end;

given x being set such that A17: ( x in dom p1 & y = p1 . x ) ; :: thesis: y in {X,Y}
x in Seg (len p1) by A17, FINSEQ_1:def 3;
then consider x' being Element of NAT such that
A18: ( x' = x & 1 <= x' & x' <= len p1 ) ;
x' in dom p1 by A18, FINSEQ_3:27;
then ( p1 . x' = <*X,Y*> . (f1 . x') & ( f1 . x' = 1 or f1 . x' = 2 ) ) by A11, A12;
hence y in {X,Y} by A3, A17, A18, TARSKI:def 2; :: thesis: verum

end;

then rng p1 = {X,Y} by FUNCT_1:def 5;
then reconsider p1 = p1 as TwoValued FinSequence by A1, A2, A12, Th19;

now

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len p1 implies p1 . i <> p1 . (i + 1) )
assume that
A19: 1 <= i and
A20: i + 1 <= len p1 ; :: thesis: p1 . i <> p1 . (i + 1)
( 1 <= i & i <= n & 1 <= i + 1 & i + 1 <= n ) by A12, A19, A20, NAT_1:13;
then ( i in dom p1 & i + 1 in dom p1 ) by A12, FINSEQ_3:27;
then ( p1 . i = <*X,Y*> . (f1 . i) & p1 . (i + 1) = <*X,Y*> . (f1 . (i + 1)) & ( f1 . i = 1 or f1 . i = 2 ) & ( f1 . (i + 1) = 1 or f1 . (i + 1) = 2 ) & f1 . i <> f1 . (i + 1) ) by A11, A12;
hence p1 . i <> p1 . (i + 1) by A1, A3; :: 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 A13, FUNCT_1:def 5; :: 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:27;
hence p1 . 1 = X by A3, A5, A12; :: thesis: verum