let i be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum