let n, k be Nat; 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; 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); ( 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
; 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 S1[ 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 S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A9:
S1[
i]
;
S1[i + 1]
assume that A10:
i + 1
in dom f
and A11:
i + 1
<= n
;
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;
( 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)) )
;
m <= k
now m <= kper cases
( i = 0 or i <> 0 )
;
suppose A13:
i <> 0
;
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 ( ( i2 < k & m <= k ) or ( i2 = k & contradiction ) )end; hence
m <= k
;
verum end; end; end;
hence
m <= k
;
verum
end;
A28:
S1[ 0 ]
by FINSEQ_3:25;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A28, A8); verum