let X, Y be set ; 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; ( 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
; 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;
( S1[i] implies S1[i + 1] )
assume that A9:
(
f1 . i = 1 or
f1 . i = 2 )
and
f1 . i <> f1 . (i + 1)
;
S1[i + 1]
thus
(
f1 . (i + 1) = 1 or
f1 . (i + 1) = 2 )
by A6, A4, A7, A9;
f1 . (i + 1) <> f1 . ((i + 1) + 1)
hence
f1 . (i + 1) <> f1 . ((i + 1) + 1)
by A6, A4, A7;
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 FINSEQ_1:sch 2();
A13:
f1 . (0 + 1) = 1
by A6, A4;
then A14:
f1 . (1 + 1) = 2
by A6, A7;
A15:
now 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 ;
( ( 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 ( ex x being object st
( x in dom p1 & y = p1 . x ) implies y in {X,Y} )
assume
y in {X,Y}
;
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;
verum
end; given x being
object such that A20:
x in dom p1
and A21:
y = p1 . x
;
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;
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 for i being Nat st 1 <= i & i + 1 <= len p1 holds
p1 . i <> p1 . (i + 1)let i be
Nat;
( 1 <= i & i + 1 <= len p1 implies p1 . i <> p1 . (i + 1) )assume that A26:
1
<= i
and A27:
i + 1
<= len p1
;
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;
verum end;
then reconsider p1 = p1 as TwoValued Alternating FinSequence by Def4;
take
p1
; ( rng p1 = {X,Y} & len p1 = n & p1 . 1 = X )
thus
rng p1 = {X,Y}
by A15, FUNCT_1:def 3; ( len p1 = n & p1 . 1 = X )
thus
len p1 = n
by A12; p1 . 1 = X
1 in dom p1
by A2, A12, FINSEQ_3:25;
hence
p1 . 1 = X
by A3, A13, A12; verum