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 (Col G,(width G)) ) and
A2: f is_sequence_on G and
A3: i in Seg (width G) and
A4: i + 1 in Seg (width G) and
A5: m in dom f and
A6: f /. m in rng (Col G,i) and
A7: for k being Element of NAT st k in dom f & f /. k in rng (Col 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 Seg (width G) & f /. n in rng (Col 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 Seg (width G) or not f /. n in rng (Col 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 Seg (width G) holds
not f /. n in rng (Col 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 (Col G,j) & (Col G,j) . i = G * i,j & i in Seg (len (Col G,j)) ) by A8, A11, MATRIX_1:def 9;
then i in dom (Col G,j) by FINSEQ_1:def 3;
hence contradiction by A12, A13, FUNCT_1:def 5; :: thesis:

end;

defpred S₁[ Nat, set ] means ( $2 in Seg (width G) & ( for k being Element of NAT st k = $2 holds
f /. $1 in rng (Col 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 Seg (width G) & f /. n in rng (Col G,k) ) by A9;
take r = k; :: thesis:
thus r in Seg (width G) by A15; :: thesis:
let m be Element of NAT ; :: thesis:
assume m = r ; :: thesis:
hence f /. n in rng (Col 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 & Seg (width 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;
A21: v <> {} by A1, A18;
A22: rng v c= Seg (width 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 Seg (width G) by A16, A17; :: thesis:

end;

A23: v . (len v) = width G

proof

assume A24: v . (len v) <> width G ; :: thesis:
A25: ( v . (len v) in Seg (width G) & ( for k being Element of NAT st k = v . (len v) holds
f /. (len v) in rng (Col G,k) ) ) by A17, A18, A19, A20;
then reconsider k = v . (len v) as Element of NAT ;
A26: f /. (len f) in rng (Col G,k) by A17, A18, A19, A20;
0 < width G by Lm1;
then 0 + 1 <= width G by NAT_1:13;
then width G in Seg (width G) by FINSEQ_1:3;
hence contradiction by A1, A24, A25, A26, Th20; :: 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 Seg (width G) & s in Seg (width G) ) by A22;
then reconsider n1 = r, n2 = s as Element of NAT ;
set L1 = Col G,n1;
set L2 = Col G,n2;
A32: ( dom (Col G,n1) = Seg (len (Col G,n1)) & dom (Col G,n2) = Seg (len (Col G,n2)) ) by FINSEQ_1:def 3;
A33: ( f /. k in rng (Col G,n1) & f /. (k + 1) in rng (Col G,n2) ) by A17, A19, A29, A30;
then consider x being Nat such that
A34: ( x in dom (Col G,n1) & (Col G,n1) . x = f /. k ) by FINSEQ_2:11;
A35: ( len (Col G,n1) = len G & len (Col G,n2) = len G ) by MATRIX_1:def 9;
then A36: f /. k = G * x,n1 by A8, A32, A34, MATRIX_1:def 9;
consider y being Nat such that
A37: ( y in dom (Col G,n2) & (Col 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 * y,n2 by A8, A32, A35, A37, MATRIX_1:def 9;
( [x,n1] in [:(dom G),(Seg (width G)):] & [y,n2] in [:(dom G),(Seg (width G)):] ) by A8, A22, A31, A32, A34, A35, A37, ZFMISC_1:106;
then ( [x,n1] in Indices G & [y,n2] in Indices G ) by MATRIX_1:def 5;
then (abs (x - y)) + (abs (n1 - n2)) = 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 Seg (width G) & ( for k being Element of NAT st k = v . m holds
f /. m in rng (Col G,k) ) ) by A5, A17, A19;
then reconsider k = v . m as Element of NAT ;
f /. m in rng (Col G,k) by A5, A17, A19;
hence contradiction by A3, A6, A40, A41, Th20; :: 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 (Col 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, A16, A19, A21, A22, A23, A27, A39, Th14;
thus m + 1 in dom f by A3, A4, A5, A16, A19, A21, A22, A23, A27, A39, A42, Th14; :: thesis:
thus f /. (m + 1) in rng (Col G,(i + 1)) by A16, A17, A44; :: thesis: