let k, n be Element of 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 Element of NAT st i in dom f & f /. i in rng (Col G,k) holds
n <= i ) holds
for i being Element of NAT st i in dom f & i <= n holds
for m being Element of 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 Element of NAT st i in dom f & f /. i in rng (Col G,k) holds
n <= i ) holds
for i being Element of NAT st i in dom f & i <= n holds
for m being Element of 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 Element of NAT st i in dom f & f /. i in rng (Col G,k) holds
n <= i ) implies for i being Element of NAT st i in dom f & i <= n holds
for m being Element of 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 Element of NAT st i in dom f & f /. i in rng (Col G,k) holds
n <= i ; :: thesis: for i being Element of NAT st i in dom f & i <= n holds
for m being Element of NAT st m in Seg (width G) & f /. i in rng (Col G,m) holds
m <= k
defpred S₁[ Element of NAT ] means ( $1 in dom f & $1 <= n implies for m being Element of 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 Lm1;
then 0 + 1 <= width G by NAT_1:13;
then A6: 1 in Seg (width G) by FINSEQ_1:3;
A7: 1 <= k by A1, FINSEQ_1:3;
A8: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of 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 Element of NAT st m in Seg (width G) & f /. (i + 1) in rng (Col G,m) holds
m <= k
let m be Element of 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

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: m <= k

hence m <= k by A2, A6, A7, A12, Th20; :: thesis: verum

end;

suppose A13: i <> 0 ; :: thesis: m <= k

i + 1 <= len f by A10, FINSEQ_3:27;
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:27;
then consider i1, i2 being Element of NAT such that
A18: [i1,i2] in Indices G and
A19: f /. i = G * i1,i2 by A3, Def11;
A20: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_1:def 5;
then A21: i2 in Seg (width G) by A18, ZFMISC_1:106;
A22: ( dom (Col G,i2) = Seg (len (Col G,i2)) & len (Col G,i2) = len G ) by FINSEQ_1:def 3, MATRIX_1:def 9;
A23: i1 in dom G by A18, A20, ZFMISC_1:106;
then (Col G,i2) . i1 = f /. i by A19, MATRIX_1:def 9;
then A24: f /. i in rng (Col G,i2) by A5, A23, A22, FUNCT_1:def 5;
then A25: i2 <= k by A9, A11, A16, A14, A21, FINSEQ_3:27, NAT_1:13;

now

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

case A26: i2 < k ; :: thesis: m <= k

now

per cases ( f /. (i + 1) in rng (Col G,i2) or for j being Element of NAT st f /. (i + 1) in rng (Col G,j) & j in Seg (width G) holds
abs (i2 - j) = 1 ) by A3, A10, A17, A21, A24, Th47;

suppose f /. (i + 1) in rng (Col G,i2) ; :: thesis: m <= k

hence m <= k by A12, A21, A26, Th20; :: thesis: verum

end;

suppose for j being Element of NAT st f /. (i + 1) in rng (Col G,j) & j in Seg (width G) holds
abs (i2 - j) = 1 ; :: thesis: m <= k

then A27: abs (i2 - m) = 1 by A12;

now

per cases ( ( i2 > m & i2 = m + 1 ) or ( i2 < m & m = i2 + 1 ) ) by A27, Th1;

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:27;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A28, A8); :: thesis: verum