let n, i be Nat; :: thesis: for G being Go-board
for f being FinSequence of () st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg () & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1

let G be Go-board; :: thesis: for f being FinSequence of () st f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg () & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1

let f be FinSequence of (); :: thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in Seg () & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) implies for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(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 () & f /. i in rng (Col (G,n)) ) ; :: thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 )

consider j1, j2 being Nat such that
A5: [j1,j2] in Indices G and
A6: f /. (i + 1) = G * (j1,j2) by A1, A3;
A7: Indices G = [:(dom G),(Seg ()):] by MATRIX_0:def 4;
then A8: j1 in dom G by ;
A9: j2 in Seg () by ;
len (Col (G,j2)) = len G by MATRIX_0:def 8;
then A10: j1 in dom (Col (G,j2)) by ;
consider i1, i2 being Nat such that
A11: [i1,i2] in Indices G and
A12: f /. i = G * (i1,i2) by A1, A2;
A13: i1 in dom G by ;
len (Col (G,i2)) = len G by MATRIX_0:def 8;
then A14: i1 in dom (Col (G,i2)) by ;
(Col (G,i2)) . i1 = f /. i by ;
then A15: f /. i in rng (Col (G,i2)) by ;
i2 in Seg () by ;
then i2 = n by A4, A15, Th3;
then A16: |.(i1 - j1).| + |.(n - j2).| = 1 by A1, A2, A3, A11, A12, A5, A6;
A17: (Col (G,j2)) . j1 = f /. (i + 1) by ;
then A18: f /. (i + 1) in rng (Col (G,j2)) by ;
now :: thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 )
per cases ( ( |.(i1 - j1).| = 1 & n = j2 ) or ( |.(n - j2).| = 1 & i1 = j1 ) ) by ;
suppose ( |.(i1 - j1).| = 1 & n = j2 ) ; :: thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 )

hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 ) by ; :: thesis: verum
end;
suppose ( |.(n - j2).| = 1 & i1 = j1 ) ; :: thesis: ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 )

hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 ) by A9, A18, Th3; :: thesis: verum
end;
end;
end;
hence ( f /. (i + 1) in rng (Col (G,n)) or for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg () holds
|.(n - k).| = 1 ) ; :: thesis: verum