let i, n be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i + 1 in dom f and
A4: ( n in dom G & f /. i in rng (Line G,n) ) ; :: thesis:
consider j1, j2 being Element of NAT such that
A5: [j1,j2] in Indices G and
A6: f /. (i + 1) = G * j1,j2 by A1, A3, Def11;
A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A8: j1 in dom G by A5, ZFMISC_1:106;
consider i1, i2 being Element of NAT such that
A9: [i1,i2] in Indices G and
A10: f /. i = G * i1,i2 by A1, A2, Def11;
A11: i2 in Seg (width G) by A9, A7, ZFMISC_1:106;
len (Line G,i1) = width G by MATRIX_1:def 8;
then A12: i2 in dom (Line G,i1) by A11, FINSEQ_1:def 3;
(Line G,i1) . i2 = f /. i by A10, A11, MATRIX_1:def 8;
then A13: f /. i in rng (Line G,i1) by A12, FUNCT_1:def 5;
i1 in dom G by A9, A7, ZFMISC_1:106;
then i1 = n by A4, A13, Th19;
then A14: (abs (n - j1)) + (abs (i2 - j2)) = 1 by A1, A2, A3, A9, A10, A5, A6, Def11;
A15: j2 in Seg (width G) by A5, A7, ZFMISC_1:106;
len (Line G,j1) = width G by MATRIX_1:def 8;
then A16: j2 in dom (Line G,j1) by A15, FINSEQ_1:def 3;
A17: (Line G,j1) . j2 = f /. (i + 1) by A6, A15, MATRIX_1:def 8;
then A18: f /. (i + 1) in rng (Line G,j1) by A16, FUNCT_1:def 5;

per cases by A14, Th2;

suppose ( abs (n - j1) = 1 & i2 = j2 ) ; :: thesis:

hence ( f /. (i + 1) in rng (Line G,n) or for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1 ) by A8, A18, Th19; :: thesis:

end;

suppose ( abs (i2 - j2) = 1 & n = j1 ) ; :: thesis:

hence ( f /. (i + 1) in rng (Line G,n) or for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1 ) by A17, A16, FUNCT_1:def 5; :: thesis:

end;

end;

end;

hence ( f /. (i + 1) in rng (Line G,n) or for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1 ) ; :: thesis: