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_{1}[ 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_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by FINSEQ_3:25;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A28, A8); :: thesis: verum

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

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

S

proof

A28:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A9: S_{1}[i]
; :: thesis: S_{1}[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

end;assume A9: S

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 <= kend;

hence
m <= k
; :: thesis: verumper cases
( i = 0 or i <> 0 )
;

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;

end;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 ) )end;

hence
m <= k
; :: thesis: verumper cases
( i2 < k or i2 = k )
by A25, XXREAL_0:1;

end;

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

end;

now :: thesis: m <= kend;

hence
m <= k
; :: thesis: verumper 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;

|.(i2 - j).| = 1 ) by A3, A10, A17, A21, A24, Th24;

end;

thus for n being Nat holds S