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 Seg (width G) & f /. i in rng (Col G,n) & not f /. (i + 1) in rng (Col G,n) holds
for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width 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 Seg (width G) & f /. i in rng (Col G,n) & not f /. (i + 1) in rng (Col G,n) holds
for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width 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 Seg (width G) & f /. i in rng (Col G,n) & not f /. (i + 1) in rng (Col G,n) implies for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width G) holds
abs (n - k) = 1 )
assume A1: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col G,n) ) ; :: thesis: ( f /. (i + 1) in rng (Col G,n) or for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width 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: ( (Col G,i2) . i1 = f /. i & len (Col G,i2) = len G & (Col G,j2) . j1 = f /. (i + 1) & len (Col G,j2) = len G ) by A2, A3, MATRIX_1:def 9;
then A6: ( i1 in dom (Col G,i2) & j1 in dom (Col G,j2) ) by A4, FINSEQ_3:31;
then A7: ( f /. i in rng (Col G,i2) & f /. (i + 1) in rng (Col G,j2) ) by A5, FUNCT_1:def 5;
then i2 = n by A1, A4, Th20;
then A8: (abs (i1 - j1)) + (abs (n - j2)) = 1 by A1, A2, A3, Def11;

now

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

suppose ( abs (i1 - j1) = 1 & n = j2 ) ; :: thesis: ( f /. (i + 1) in rng (Col G,n) or for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width G) holds
abs (n - k) = 1 )

hence ( f /. (i + 1) in rng (Col G,n) or for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width G) holds
abs (n - k) = 1 ) by A5, A6, FUNCT_1:def 5; :: thesis: verum

end;

suppose ( abs (n - j2) = 1 & i1 = j1 ) ; :: thesis: ( f /. (i + 1) in rng (Col G,n) or for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width G) holds
abs (n - k) = 1 )

hence ( f /. (i + 1) in rng (Col G,n) or for k being Element of NAT st f /. (i + 1) in rng (Col G,k) & k in Seg (width G) holds
abs (n - k) = 1 ) by A4, A7, Th20; :: thesis: verum

end;

end;

end;

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