let m, i be Nat; for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Nat st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
let G be Go-board; for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Nat st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
let f be FinSequence of (TOP-REAL 2); ( 1 <= len f & f /. (len f) in rng (Col (G,(width G))) & f is_sequence_on G & i in Seg (width G) & i + 1 in Seg (width G) & m in dom f & f /. m in rng (Col (G,i)) & ( for k being Nat st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m ) implies ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) ) )
assume that
A1:
1 <= len f
and
A2:
f /. (len f) in rng (Col (G,(width G)))
and
A3:
f is_sequence_on G
and
A4:
i in Seg (width G)
and
A5:
i + 1 in Seg (width G)
and
A6:
m in dom f
and
A7:
f /. m in rng (Col (G,i))
and
A8:
for k being Nat st k in dom f & f /. k in rng (Col (G,i)) holds
k <= m
; ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )
defpred S1[ Nat, set ] means ( $2 in Seg (width G) & ( for k being Nat st k = $2 holds
f /. $1 in rng (Col (G,k)) ) );
A9:
dom G = Seg (len G)
by FINSEQ_1:def 3;
A10:
for n being Nat st n in dom f holds
ex k being Nat st
( k in Seg (width G) & f /. n in rng (Col (G,k)) )
proof
assume
ex
n being
Nat st
(
n in dom f & ( for
k being
Nat holds
( not
k in Seg (width G) or not
f /. n in rng (Col (G,k)) ) ) )
;
contradiction
then consider n being
Nat such that A11:
n in dom f
and A12:
for
k being
Nat st
k in Seg (width G) holds
not
f /. n in rng (Col (G,k))
;
consider i,
j being
Nat such that A13:
[i,j] in Indices G
and A14:
f /. n = G * (
i,
j)
by A3, A11;
A15:
[i,j] in [:(dom G),(Seg (width G)):]
by A13, MATRIX_0:def 4;
then
j in Seg (width G)
by ZFMISC_1:87;
then A16:
not
f /. n in rng (Col (G,j))
by A12;
A17:
i in dom G
by A15, ZFMISC_1:87;
then
i in Seg (len (Col (G,j)))
by A9, MATRIX_0:def 8;
then A18:
i in dom (Col (G,j))
by FINSEQ_1:def 3;
(Col (G,j)) . i = G * (
i,
j)
by A17, MATRIX_0:def 8;
hence
contradiction
by A14, A16, A18, FUNCT_1:def 3;
verum
end;
A19:
for n being Nat st n in Seg (len f) holds
ex r being Element of REAL st S1[n,r]
consider v being FinSequence of REAL such that
A22:
dom v = Seg (len f)
and
A23:
for n being Nat st n in Seg (len f) holds
S1[n,v . n]
from FINSEQ_1:sch 5(A19);
A24:
dom f = Seg (len f)
by FINSEQ_1:def 3;
A25:
for k being Nat st k in dom v & v . k = i holds
k <= m
A28:
rng v c= Seg (width G)
A29:
len v = len f
by A22, FINSEQ_1:def 3;
A30:
for k being Nat st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s
proof
let k be
Nat;
( 1 <= k & k <= (len v) - 1 implies for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s )
assume that A31:
1
<= k
and A32:
k <= (len v) - 1
;
for r, s being Real st r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 holds
r = s
A33:
k + 1
<= len v
by A32, XREAL_1:19;
let r,
s be
Real;
( r = v . k & s = v . (k + 1) & not |.(r - s).| = 1 implies r = s )
assume that A34:
r = v . k
and A35:
s = v . (k + 1)
;
( |.(r - s).| = 1 or r = s )
1
<= k + 1
by NAT_1:11;
then A36:
k + 1
in dom f
by A29, A33, FINSEQ_3:25;
then A37:
s in rng v
by A22, A24, A35, FUNCT_1:def 3;
then A38:
s in Seg (width G)
by A28;
k <= k + 1
by NAT_1:11;
then
k <= len f
by A29, A33, XXREAL_0:2;
then A39:
k in dom f
by A31, FINSEQ_3:25;
then A40:
r in rng v
by A22, A24, A34, FUNCT_1:def 3;
then
r in Seg (width G)
by A28;
then reconsider n1 =
r,
n2 =
s as
Element of
NAT by A38;
set L1 =
Col (
G,
n1);
set L2 =
Col (
G,
n2);
f /. k in rng (Col (G,n1))
by A23, A24, A39, A34;
then consider x being
Nat such that A41:
x in dom (Col (G,n1))
and A42:
(Col (G,n1)) . x = f /. k
by FINSEQ_2:10;
A43:
(
dom (Col (G,n1)) = Seg (len (Col (G,n1))) &
len (Col (G,n1)) = len G )
by FINSEQ_1:def 3, MATRIX_0:def 8;
then A44:
f /. k = G * (
x,
n1)
by A9, A41, A42, MATRIX_0:def 8;
f /. (k + 1) in rng (Col (G,n2))
by A23, A24, A36, A35;
then consider y being
Nat such that A45:
y in dom (Col (G,n2))
and A46:
(Col (G,n2)) . y = f /. (k + 1)
by FINSEQ_2:10;
reconsider x =
x,
y =
y as
Element of
NAT by ORDINAL1:def 12;
[x,n1] in [:(dom G),(Seg (width G)):]
by A9, A28, A40, A41, A43, ZFMISC_1:87;
then A47:
[x,n1] in Indices G
by MATRIX_0:def 4;
A48:
(
dom (Col (G,n2)) = Seg (len (Col (G,n2))) &
len (Col (G,n2)) = len G )
by FINSEQ_1:def 3, MATRIX_0:def 8;
then
[y,n2] in [:(dom G),(Seg (width G)):]
by A9, A28, A37, A45, ZFMISC_1:87;
then A49:
[y,n2] in Indices G
by MATRIX_0:def 4;
f /. (k + 1) = G * (
y,
n2)
by A9, A48, A45, A46, MATRIX_0:def 8;
then
|.(x - y).| + |.(n1 - n2).| = 1
by A3, A39, A36, A44, A47, A49;
hence
(
|.(r - s).| = 1 or
r = s )
by SEQM_3:42;
verum
end;
A50:
v . m = i
( 1 <= m & m <= len f )
by A6, FINSEQ_3:25;
then
1 <= len f
by XXREAL_0:2;
then A53:
len f in dom f
by FINSEQ_3:25;
A54:
v . (len v) = width G
proof
0 < width G
by MATRIX_0:44;
then
0 + 1
<= width G
by NAT_1:13;
then A55:
width G in Seg (width G)
by FINSEQ_1:1;
A56:
v . (len v) in Seg (width G)
by A23, A29, A24, A53;
then reconsider k =
v . (len v) as
Element of
NAT ;
assume A57:
v . (len v) <> width G
;
contradiction
f /. (len f) in rng (Col (G,k))
by A23, A29, A24, A53;
hence
contradiction
by A2, A57, A56, A55, Th3;
verum
end;
A58:
v <> {}
by A1, A22;
hence
m + 1 in dom f
by A4, A5, A6, A22, A24, A28, A54, A30, A50, A25, SEQM_3:45; f /. (m + 1) in rng (Col (G,(i + 1)))
( m + 1 in dom v & v . (m + 1) = i + 1 )
by A4, A5, A6, A22, A24, A58, A28, A54, A30, A50, A25, SEQM_3:45;
hence
f /. (m + 1) in rng (Col (G,(i + 1)))
by A22, A23; verum