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 that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i + 1 in dom f and
A4: ( 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 )
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;
A9: j2 in Seg (width G) by A5, A7, ZFMISC_1:106;
len (Col G,j2) = len G by MATRIX_1:def 9;
then A10: j1 in dom (Col G,j2) by A8, FINSEQ_3:31;
consider i1, i2 being Element of NAT such that
A11: [i1,i2] in Indices G and
A12: f /. i = G * i1,i2 by A1, A2, Def11;
A13: i1 in dom G by A11, A7, ZFMISC_1:106;
len (Col G,i2) = len G by MATRIX_1:def 9;
then A14: i1 in dom (Col G,i2) by A13, FINSEQ_3:31;
(Col G,i2) . i1 = f /. i by A12, A13, MATRIX_1:def 9;
then A15: f /. i in rng (Col G,i2) by A14, FUNCT_1:def 5;
i2 in Seg (width G) by A11, A7, ZFMISC_1:106;
then i2 = n by A4, A15, Th20;
then A16: (abs (i1 - j1)) + (abs (n - j2)) = 1 by A1, A2, A3, A11, A12, A5, A6, Def11;
A17: (Col G,j2) . j1 = f /. (i + 1) by A6, A8, MATRIX_1:def 9;
then A18: f /. (i + 1) in rng (Col G,j2) by A10, FUNCT_1:def 5;

now

per cases ( ( abs (i1 - j1) = 1 & n = j2 ) or ( abs (n - j2) = 1 & i1 = j1 ) ) by A16, 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 A17, A10, 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 A9, A18, 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