let i be Nat; for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Nat st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
let G be Go-board; for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Nat st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
let f be FinSequence of (TOP-REAL 2); ( f is_sequence_on G & i in dom f implies ex n being Nat st
( n in Seg (width G) & f /. i in rng (Col (G,n)) ) )
assume
( f is_sequence_on G & i in dom f )
; ex n being Nat st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )
then consider n, m being Nat such that
A1:
[n,m] in Indices G
and
A2:
f /. i = G * (n,m)
;
set L = Col (G,m);
take
m
; ( m in Seg (width G) & f /. i in rng (Col (G,m)) )
A3:
Indices G = [:(dom G),(Seg (width G)):]
by MATRIX_0:def 4;
hence
m in Seg (width G)
by A1, ZFMISC_1:87; f /. i in rng (Col (G,m))
A4:
n in dom G
by A1, A3, ZFMISC_1:87;
len (Col (G,m)) = len G
by MATRIX_0:def 8;
then A5:
n in dom (Col (G,m))
by A4, FINSEQ_3:29;
(Col (G,m)) . n = f /. i
by A2, A4, MATRIX_0:def 8;
hence
f /. i in rng (Col (G,m))
by A5, FUNCT_1:def 3; verum