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 dom G & f /. i in rng (Line (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 dom G & f /. i in rng (Line (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 dom G & f /. i in rng (Line (G,n)) ) )
assume ( f is_sequence_on G & i in dom f ) ; :: thesis: ex n being Nat st
( n in dom G & f /. i in rng (Line (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 = Line (G,n);
take n ; :: thesis: ( n in dom G & f /. i in rng (Line (G,n)) )
A3: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;
hence n in dom G by A1, ZFMISC_1:87; :: thesis: f /. i in rng (Line (G,n))
A4: m in Seg (width G) by A1, A3, ZFMISC_1:87;
len (Line (G,n)) = width G by MATRIX_0:def 7;
then A5: m in dom (Line (G,n)) by A4, FINSEQ_1:def 3;
(Line (G,n)) . m = f /. i by A2, A4, MATRIX_0:def 7;
hence f /. i in rng (Line (G,n)) by A5, FUNCT_1:def 3; :: thesis: verum