let n, k be Nat; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & 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 (width G) & f /. i in rng (Col (G,m)) holds
m <= k
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st k in Seg (width G) & 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 (width G) & f /. i in rng (Col (G,m)) holds
m <= k
let f be FinSequence of (TOP-REAL 2); :: thesis: ( k in Seg (width G) & 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 (width G) & f /. i in rng (Col (G,m)) holds
m <= k )
assume that
A1: k in Seg (width G) 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 (width G) & f /. i in rng (Col (G,m)) holds
m <= k
defpred S₁[ Nat] means ( $1 in dom f & $1 <= n implies for m being Nat st m in Seg (width G) & 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 (width G) by FINSEQ_1:1;
A7: 1 <= k by A1, FINSEQ_1:1;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: S₁[i] ; :: thesis: S₁[i + 1]
assume that
A10: i + 1 in dom f and
A11: i + 1 <= n ; :: thesis: for m being Nat st m in Seg (width G) & f /. (i + 1) in rng (Col (G,m)) holds
m <= k
let m be Nat; :: thesis: ( m in Seg (width G) & f /. (i + 1) in rng (Col (G,m)) implies m <= k )
assume A12: ( m in Seg (width G) & 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 A10, FINSEQ_3:25;
then A14: i <= len f by NAT_1:13;
A15: i < n by A11, NAT_1:13;
A16: 0 + 1 <= i by A13, NAT_1:13;
then A17: i in dom f by A14, FINSEQ_3:25;
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 (width G)):] by MATRIX_0:def 4;
then A21: i2 in Seg (width G) by A18, ZFMISC_1:87;
A22: ( dom (Col (G,i2)) = Seg (len (Col (G,i2))) & len (Col (G,i2)) = len G ) by FINSEQ_1:def 3, MATRIX_0:def 8;
A23: i1 in dom G by A18, A20, ZFMISC_1:87;
then (Col (G,i2)) . i1 = f /. i by A19, MATRIX_0:def 8;
then A24: f /. i in rng (Col (G,i2)) by A5, A23, A22, FUNCT_1:def 3;
then A25: i2 <= k by A9, A11, A16, A14, A21, FINSEQ_3:25, NAT_1:13;

now :: thesis: ( ( i2 < k & m <= k ) or ( i2 = k & contradiction ) )

per cases ( i2 < k or i2 = k ) by A25, XXREAL_0:1;

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 (width G) 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 (width G) 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 A27, SEQM_3:41;

suppose ( i2 > m & i2 = m + 1 ) ; :: thesis: m <= k

hence m <= k by A26, XXREAL_0:2; :: thesis: verum

end;

suppose ( i2 < m & m = i2 + 1 ) ; :: thesis: m <= k

hence m <= k by A26, NAT_1:13; :: thesis: verum

end;

end;

end;

hence m <= k ; :: thesis: verum

end;

end;

end;

hence m <= k ; :: thesis: verum

end;

case i2 = k ; :: thesis: contradiction

hence contradiction by A4, A15, A17, A24; :: thesis: verum

end;

end;

end;

hence m <= k ; :: thesis: verum

end;

end;

end;

hence m <= k ; :: thesis: verum

end;

A28: S₁[ 0 ] by FINSEQ_3:25;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A28, A8); :: thesis: verum