let i, m be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: ( 1 <= len f & f /. (len f) in rng (Line G,(len G)) ) and
A2: f is_sequence_on G and
A3: i in dom G and
A4: i + 1 in dom G and
A5: m in dom f and
A6: f /. m in rng (Line G,i) and
A7: for k being Element of NAT st k in dom f & f /. k in rng (Line G,i) holds
k <= m ; :: thesis:
A8: dom G = Seg (len G) by FINSEQ_1:def 3;
A9: for n being Element of NAT st n in dom f holds
ex k being Element of NAT st
( k in dom G & f /. n in rng (Line G,k) )

proof

assume ex n being Element of NAT st
( n in dom f & ( for k being Element of NAT holds
( not k in dom G or not f /. n in rng (Line G,k) ) ) ) ; :: thesis:
then consider n being Element of NAT such that
A10: n in dom f and
A11: for k being Element of NAT st k in dom G holds
not f /. n in rng (Line G,k) ;
consider i, j being Element of NAT such that
A12: ( [i,j] in Indices G & f /. n = G * i,j ) by A2, A10, Def11;
[i,j] in [:(dom G),(Seg (width G)):] by A12, MATRIX_1:def 5;
then ( i in dom G & j in Seg (width G) ) by ZFMISC_1:106;
then A13: ( not f /. n in rng (Line G,i) & (Line G,i) . j = G * i,j & j in Seg (len (Line G,i)) ) by A11, MATRIX_1:def 8;
then j in dom (Line G,i) by FINSEQ_1:def 3;
hence contradiction by A12, A13, FUNCT_1:def 5; :: thesis:

end;

defpred S₁[ Nat, set ] means ( $2 in dom G & ( for k being Element of NAT st k = $2 holds
f /. $1 in rng (Line G,k) ) );
A14: for n being Nat st n in Seg (len f) holds
ex r being Real st S₁[n,r]

proof

let n be Nat; :: thesis:
assume n in Seg (len f) ; :: thesis:
then n in dom f by FINSEQ_1:def 3;
then consider k being Element of NAT such that
A15: ( k in dom G & f /. n in rng (Line G,k) ) by A9;
take r = k; :: thesis:
thus r in dom G by A15; :: thesis:
let m be Element of NAT ; :: thesis:
assume m = r ; :: thesis:
hence f /. n in rng (Line G,m) by A15; :: thesis:

end;

consider v being FinSequence of REAL such that
A16: dom v = Seg (len f) and
A17: for n being Nat st n in Seg (len f) holds
S₁[n,v . n] from FINSEQ_1:sch 5(A14);
A18: len v = len f by A16, FINSEQ_1:def 3;
A19: ( dom v = Seg (len v) & dom f = Seg (len f) & dom f c= NAT & dom G c= NAT ) by FINSEQ_1:def 3;
( 1 <= m & m <= len f ) by A5, FINSEQ_3:27;
then ( 1 <= 1 & 1 <= len f & len f <= len f ) by XXREAL_0:2;
then A20: ( 1 in dom f & len f in dom f ) by FINSEQ_3:27;
reconsider p = f /. (len f), q = f /. m as Point of (TOP-REAL 2) ;
A21: v <> {} by A1, A18;
A22: rng v c= dom G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng v ; :: thesis:
then ex y being Nat st
( y in dom v & v . y = x ) by FINSEQ_2:11;
hence x in dom G by A16, A17; :: thesis:

end;

A23: v . (len v) = len G

proof

assume A24: v . (len v) <> len G ; :: thesis:
A25: ( v . (len v) in dom G & ( for k being Element of NAT st k = v . (len v) holds
f /. (len v) in rng (Line G,k) ) ) by A17, A18, A19, A20;
then reconsider k = v . (len v) as Element of NAT ;
A26: p in rng (Line G,k) by A17, A18, A19, A20;
0 < len G by Lm1;
then ( 0 + 1 <= len G & len G <= len G ) by NAT_1:13;
then len G in dom G by FINSEQ_3:27;
hence contradiction by A1, A24, A25, A26, Th19; :: thesis:

end;

A27: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s

proof

let k be Element of NAT ; :: thesis:
assume A28: ( 1 <= k & k <= (len v) - 1 ) ; :: thesis:
then ( k <= k + 1 & k + 1 <= len v ) by NAT_1:11, XREAL_1:21;
then ( 1 <= k + 1 & k + 1 <= len f & 1 <= k & k <= len f ) by A18, A28, XXREAL_0:2;
then A29: ( k in dom f & k + 1 in dom f ) by FINSEQ_3:27;
let r, s be Real; :: thesis:
assume A30: ( r = v . k & s = v . (k + 1) ) ; :: thesis:
then A31: ( r in rng v & s in rng v ) by A16, A19, A29, FUNCT_1:def 5;
then ( r in dom G & s in dom G ) by A22;
then reconsider n1 = r, n2 = s as Element of NAT ;
set L1 = Line G,n1;
set L2 = Line G,n2;
A32: ( dom (Line G,n1) = Seg (len (Line G,n1)) & Seg (len (Line G,n2)) = dom (Line G,n2) ) by FINSEQ_1:def 3;
A33: ( f /. k in rng (Line G,n1) & f /. (k + 1) in rng (Line G,n2) ) by A17, A19, A29, A30;
then consider x being Nat such that
A34: ( x in dom (Line G,n1) & (Line G,n1) . x = f /. k ) by FINSEQ_2:11;
A35: ( len (Line G,n1) = width G & len (Line G,n2) = width G ) by MATRIX_1:def 8;
then A36: f /. k = G * n1,x by A32, A34, MATRIX_1:def 8;
consider y being Nat such that
A37: ( y in dom (Line G,n2) & (Line G,n2) . y = f /. (k + 1) ) by A33, FINSEQ_2:11;
reconsider x = x, y = y as Element of NAT by ORDINAL1:def 13;
A38: f /. (k + 1) = G * n2,y by A32, A35, A37, MATRIX_1:def 8;
( [n1,x] in [:(dom G),(Seg (width G)):] & [n2,y] in [:(dom G),(Seg (width G)):] ) by A22, A31, A32, A34, A35, A37, ZFMISC_1:106;
then ( [n1,x] in Indices G & [n2,y] in Indices G ) by MATRIX_1:def 5;
then (abs (n1 - n2)) + (abs (x - y)) = 1 by A2, A29, A36, A38, Def11;
hence ( abs (r - s) = 1 or r = s ) by Th2; :: thesis:

end;

A39: v . m = i

proof

assume A40: v . m <> i ; :: thesis:
A41: ( v . m in dom G & ( for k being Element of NAT st k = v . m holds
f /. m in rng (Line G,k) ) ) by A5, A17, A19;
then reconsider k = v . m as Element of NAT ;
q in rng (Line G,k) by A5, A17, A19;
hence contradiction by A3, A6, A40, A41, Th19; :: thesis:

end;

A42: for k being Element of NAT st k in dom v & v . k = i holds
k <= m

proof

let k be Element of NAT ; :: thesis:
assume A43: ( k in dom v & v . k = i ) ; :: thesis:
then f /. k in rng (Line G,i) by A16, A17;
hence k <= m by A7, A16, A19, A43; :: thesis:

end;

then A44: ( m + 1 in dom v & v . (m + 1) = i + 1 ) by A3, A4, A5, A8, A16, A19, A21, A22, A23, A27, A39, Th14;
thus m + 1 in dom f by A3, A4, A5, A8, A16, A19, A21, A22, A23, A27, A39, A42, Th14; :: thesis:
thus f /. (m + 1) in rng (Line G,(i + 1)) by A16, A17, A44; :: thesis: