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