let m, i be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )

defpred S_{1}[ 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)) )

ex r being Element of REAL st S_{1}[n,r]

A22: dom v = Seg (len f) and

A23: for n being Nat st n in Seg (len f) holds

S_{1}[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

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

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

hence m + 1 in dom f by A4, A5, A6, A22, A24, A28, A54, A30, A50, A25, SEQM_3:45; :: thesis: 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; :: thesis: verum

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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(i + 1))) )

defpred S

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

A19:
for n being Nat st n in Seg (len f) holds
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)) ) ) ) ; :: thesis: 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; :: thesis: verum

end;( n in dom f & ( for k being Nat holds

( not k in Seg (width G) or not f /. n in rng (Col (G,k)) ) ) ) ; :: thesis: 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; :: thesis: verum

ex r being Element of REAL st S

proof

consider v being FinSequence of REAL such that
let n be Nat; :: thesis: ( n in Seg (len f) implies ex r being Element of REAL st S_{1}[n,r] )

assume n in Seg (len f) ; :: thesis: ex r being Element of REAL st S_{1}[n,r]

then n in dom f by FINSEQ_1:def 3;

then consider k being Nat such that

A20: k in Seg (width G) and

A21: f /. n in rng (Col (G,k)) by A10;

reconsider r = k as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: S_{1}[n,r]

thus r in Seg (width G) by A20; :: thesis: for k being Nat st k = r holds

f /. n in rng (Col (G,k))

let m be Nat; :: thesis: ( m = r implies f /. n in rng (Col (G,m)) )

assume m = r ; :: thesis: f /. n in rng (Col (G,m))

hence f /. n in rng (Col (G,m)) by A21; :: thesis: verum

end;assume n in Seg (len f) ; :: thesis: ex r being Element of REAL st S

then n in dom f by FINSEQ_1:def 3;

then consider k being Nat such that

A20: k in Seg (width G) and

A21: f /. n in rng (Col (G,k)) by A10;

reconsider r = k as Element of REAL by XREAL_0:def 1;

take r ; :: thesis: S

thus r in Seg (width G) by A20; :: thesis: for k being Nat st k = r holds

f /. n in rng (Col (G,k))

let m be Nat; :: thesis: ( m = r implies f /. n in rng (Col (G,m)) )

assume m = r ; :: thesis: f /. n in rng (Col (G,m))

hence f /. n in rng (Col (G,m)) by A21; :: thesis: verum

A22: dom v = Seg (len f) and

A23: for n being Nat st n in Seg (len f) holds

S

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

proof

A28:
rng v c= Seg (width G)
let k be Nat; :: thesis: ( k in dom v & v . k = i implies k <= m )

assume that

A26: k in dom v and

A27: v . k = i ; :: thesis: k <= m

f /. k in rng (Col (G,i)) by A22, A23, A26, A27;

hence k <= m by A8, A22, A24, A26; :: thesis: verum

end;assume that

A26: k in dom v and

A27: v . k = i ; :: thesis: k <= m

f /. k in rng (Col (G,i)) by A22, A23, A26, A27;

hence k <= m by A8, A22, A24, A26; :: thesis: verum

proof

A29:
len v = len f
by A22, FINSEQ_1:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng v or x in Seg (width G) )

assume x in rng v ; :: thesis: x in Seg (width G)

then ex y being Nat st

( y in dom v & v . y = x ) by FINSEQ_2:10;

hence x in Seg (width G) by A22, A23; :: thesis: verum

end;assume x in rng v ; :: thesis: x in Seg (width G)

then ex y being Nat st

( y in dom v & v . y = x ) by FINSEQ_2:10;

hence x in Seg (width G) by A22, A23; :: thesis: verum

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

A50:
v . m = i
let k be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( |.(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; :: thesis: verum

end;r = s )

assume that

A31: 1 <= k and

A32: k <= (len v) - 1 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( |.(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; :: thesis: verum

proof

( 1 <= m & m <= len f )
by A6, FINSEQ_3:25;
A51:
v . m in Seg (width G)
by A6, A23, A24;

then reconsider k = v . m as Element of NAT ;

assume A52: v . m <> i ; :: thesis: contradiction

f /. m in rng (Col (G,k)) by A6, A23, A24;

hence contradiction by A4, A7, A52, A51, Th3; :: thesis: verum

end;then reconsider k = v . m as Element of NAT ;

assume A52: v . m <> i ; :: thesis: contradiction

f /. m in rng (Col (G,k)) by A6, A23, A24;

hence contradiction by A4, A7, A52, A51, Th3; :: thesis: verum

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

A58:
v <> {}
by A1, A22;
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 ; :: thesis: contradiction

f /. (len f) in rng (Col (G,k)) by A23, A29, A24, A53;

hence contradiction by A2, A57, A56, A55, Th3; :: thesis: verum

end;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 ; :: thesis: contradiction

f /. (len f) in rng (Col (G,k)) by A23, A29, A24, A53;

hence contradiction by A2, A57, A56, A55, Th3; :: thesis: verum

hence m + 1 in dom f by A4, A5, A6, A22, A24, A28, A54, A30, A50, A25, SEQM_3:45; :: thesis: 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; :: thesis: verum