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

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

let f be FinSequence of (); :: thesis: ( k in Seg () & f /. 1 in rng (Col (G,1)) & f is_sequence_on G & ( for i being Nat st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ) implies for i being Nat st i in dom f & i <= n holds
for m being Nat st m in Seg () & f /. i in rng (Col (G,m)) holds
m <= k )

assume that
A1: k in Seg () and
A2: f /. 1 in rng (Col (G,1)) and
A3: f is_sequence_on G and
A4: for i being Nat st i in dom f & f /. i in rng (Col (G,k)) holds
n <= i ; :: thesis: for i being Nat st i in dom f & i <= n holds
for m being Nat st m in Seg () & f /. i in rng (Col (G,m)) holds
m <= k

defpred S1[ Nat] means ( \$1 in dom f & \$1 <= n implies for m being Nat st m in Seg () & f /. \$1 in rng (Col (G,m)) holds
m <= k );
A5: dom G = Seg (len G) by FINSEQ_1:def 3;
0 < width G by MATRIX_0:44;
then 0 + 1 <= width G by NAT_1:13;
then A6: 1 in Seg () by FINSEQ_1:1;
A7: 1 <= k by ;
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A9: S1[i] ; :: thesis: S1[i + 1]
assume that
A10: i + 1 in dom f and
A11: i + 1 <= n ; :: thesis: for m being Nat st m in Seg () & f /. (i + 1) in rng (Col (G,m)) holds
m <= k

let m be Nat; :: thesis: ( m in Seg () & f /. (i + 1) in rng (Col (G,m)) implies m <= k )
assume A12: ( m in Seg () & f /. (i + 1) in rng (Col (G,m)) ) ; :: thesis: m <= k
now :: thesis: m <= k
per cases ( i = 0 or i <> 0 ) ;
suppose i = 0 ; :: thesis: m <= k
hence m <= k by A2, A6, A7, A12, Th3; :: thesis: verum
end;
suppose A13: i <> 0 ; :: thesis: m <= k
i + 1 <= len f by ;
then A14: i <= len f by NAT_1:13;
A15: i < n by ;
A16: 0 + 1 <= i by ;
then A17: i in dom f by ;
then consider i1, i2 being Nat such that
A18: [i1,i2] in Indices G and
A19: f /. i = G * (i1,i2) by A3;
A20: Indices G = [:(dom G),(Seg ()):] by MATRIX_0:def 4;
then A21: i2 in Seg () by ;
A22: ( dom (Col (G,i2)) = Seg (len (Col (G,i2))) & len (Col (G,i2)) = len G ) by ;
A23: i1 in dom G by ;
then (Col (G,i2)) . i1 = f /. i by ;
then A24: f /. i in rng (Col (G,i2)) by ;
then A25: i2 <= k by ;
now :: thesis: ( ( i2 < k & m <= k ) or ( i2 = k & contradiction ) )
per cases ( i2 < k or i2 = k ) by ;
case A26: i2 < k ; :: thesis: m <= k
now :: thesis: m <= k
per cases ( f /. (i + 1) in rng (Col (G,i2)) or for j being Nat st f /. (i + 1) in rng (Col (G,j)) & j in Seg () holds
|.(i2 - j).| = 1 )
by A3, A10, A17, A21, A24, Th24;
suppose f /. (i + 1) in rng (Col (G,i2)) ; :: thesis: m <= k
hence m <= k by A12, A21, A26, Th3; :: thesis: verum
end;
suppose for j being Nat st f /. (i + 1) in rng (Col (G,j)) & j in Seg () holds
|.(i2 - j).| = 1 ; :: thesis: m <= k
then A27: |.(i2 - m).| = 1 by A12;
now :: thesis: m <= k
per cases ( ( i2 > m & i2 = m + 1 ) or ( i2 < m & m = i2 + 1 ) ) by ;
suppose ( i2 > m & i2 = m + 1 ) ; :: thesis: m <= k
hence m <= k by ; :: thesis: verum
end;
suppose ( i2 < m & m = i2 + 1 ) ; :: thesis: m <= k
hence m <= k by ; :: thesis: verum
end;
end;
end;
hence m <= k ; :: thesis: verum
end;
end;
end;
hence m <= k ; :: thesis: verum
end;
end;
end;
hence m <= k ; :: thesis: verum
end;
end;
end;
hence m <= k ; :: thesis: verum
end;
A28: S1[ 0 ] by FINSEQ_3:25;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A28, A8); :: thesis: verum