let m, i be Nat; :: thesis: for G being Go-board
for f being FinSequence of () 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; :: thesis: for f being FinSequence of () 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 (); :: thesis: ( 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 ; :: thesis: ( 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 () ;
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)) ) ) ) ; :: thesis: 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 ;
A14: [i,j] in [:(dom G),(Seg ()):] by ;
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 () by ;
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 ;
hence contradiction by A13, A15, A17, FUNCT_1:def 3; :: thesis: verum
end;
A18: for n being Nat st n in Seg (len f) holds
ex r being Element of REAL st S1[n,r]
proof
let n be Nat; :: thesis: ( n in Seg (len f) implies ex r being Element of REAL st S1[n,r] )
assume n in Seg (len f) ; :: thesis: ex r being Element of REAL st S1[n,r]
then n in dom f by FINSEQ_1:def 3;
then consider k being Nat such that
A19: k in dom G and
A20: f /. n in rng (Line (G,k)) by A9;
reconsider r = k as Element of REAL by XREAL_0:def 1;
take r ; :: thesis: S1[n,r]
thus r in dom G by A19; :: thesis: for k being Nat st k = r holds
f /. n in rng (Line (G,k))

let m be Nat; :: thesis: ( m = r implies f /. n in rng (Line (G,m)) )
assume m = r ; :: thesis: f /. n in rng (Line (G,m))
hence f /. n in rng (Line (G,m)) by A20; :: thesis: verum
end;
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 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
proof
let k be Nat; :: thesis: ( k in dom v & v . k = i implies k <= m )
assume that
A25: k in dom v and
A26: v . k = i ; :: thesis: k <= m
f /. k in rng (Line (G,i)) by A21, A22, A25, A26;
hence k <= m by A8, A21, A23, A25; :: thesis: verum
end;
A27: rng v c= dom G
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng v or x in dom G )
assume x in rng v ; :: thesis: x in dom G
then ex y being Nat st
( y in dom v & v . y = x ) by FINSEQ_2:10;
hence x in dom G by ; :: thesis: verum
end;
A28: len v = len f by ;
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; :: 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
A30: 1 <= k and
A31: 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

A32: k + 1 <= len v by ;
let r, s be Real; :: thesis: ( 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) ; :: thesis: ( |.(r - s).| = 1 or r = s )
1 <= k + 1 by NAT_1:11;
then A35: k + 1 in dom f by ;
then A36: s in rng v by ;
then A37: s in dom G by A27;
k <= k + 1 by NAT_1:11;
then k <= len f by ;
then A38: k in dom f by ;
then A39: r in rng v by ;
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 ;
then A43: f /. k = G * (n1,x) by ;
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 ()):] by ;
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 ;
then [n2,y] in [:(dom G),(Seg ()):] by ;
then A48: [n2,y] in Indices G by MATRIX_0:def 4;
f /. (k + 1) = G * (n2,y) by ;
then |.(n1 - n2).| + |.(x - y).| = 1 by A3, A38, A35, A43, A46, A48;
hence ( |.(r - s).| = 1 or r = s ) by SEQM_3:42; :: thesis: verum
end;
A49: v . m = i
proof
A50: v . m in dom G by A6, A22, A23;
then reconsider k = v . m as Element of NAT ;
assume A51: v . m <> i ; :: thesis: contradiction
q in rng (Line (G,k)) by A6, A22, A23;
hence contradiction by A4, A7, A51, A50, Th2; :: thesis: verum
end;
( 1 <= m & m <= len f ) by ;
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 ; :: thesis: contradiction
p in rng (Line (G,k)) by A22, A28, A23, A52;
hence contradiction by A2, A56, A55, A54, Th2; :: thesis: verum
end;
A57: ( dom G = Seg (len G) & v <> {} ) by ;
hence m + 1 in dom f by A4, A5, A6, A21, A23, A27, A53, A29, A49, A24, SEQM_3:45; :: thesis: 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 ; :: thesis: verum