let i, n be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line G,n) & not f /. (i + 1) in rng (Line G,n) holds
for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line G,n) & not f /. (i + 1) in rng (Line G,n) holds
for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line G,n) & not f /. (i + 1) in rng (Line G,n) implies for k being Element of NAT st f /. (i + 1) in rng (Line G,k) & k in dom G holds
abs (n - k) = 1 )
assume A1: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line G,n) ) ; :: thesis: ( 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 )
then consider i1, i2 being Element of NAT such that
A2: ( [i1,i2] in Indices G & f /. i = G * i1,i2 ) by Def11;
consider j1, j2 being Element of NAT such that
A3: ( [j1,j2] in Indices G & f /. (i + 1) = G * j1,j2 ) by A1, Def11;
Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A4: ( i1 in dom G & i2 in Seg (width G) & j1 in dom G & j2 in Seg (width G) ) by A2, A3, ZFMISC_1:106;
then A5: ( (Line G,i1) . i2 = f /. i & len (Line G,i1) = width G & (Line G,j1) . j2 = f /. (i + 1) & len (Line G,j1) = width G ) by A2, A3, MATRIX_1:def 8;
then A6: ( i2 in dom (Line G,i1) & j2 in dom (Line G,j1) ) by A4, FINSEQ_1:def 3;
then A7: ( f /. i in rng (Line G,i1) & f /. (i + 1) in rng (Line G,j1) ) by A5, FUNCT_1:def 5;
then i1 = n by A1, A4, Th19;
then A8: (abs (n - j1)) + (abs (i2 - j2)) = 1 by A1, A2, A3, Def11;

now

per cases ( ( abs (n - j1) = 1 & i2 = j2 ) or ( abs (i2 - j2) = 1 & n = j1 ) ) by A8, Th2;

suppose ( abs (n - j1) = 1 & i2 = j2 ) ; :: thesis: ( 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 )

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 A4, A7, Th19; :: thesis: verum

end;

suppose ( abs (i2 - j2) = 1 & n = j1 ) ; :: thesis: ( 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 )

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 A5, A6, FUNCT_1:def 5; :: thesis: verum

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: verum