let i be Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st
( n in dom G & f /. i in rng (Line G,n) )
then consider n, m being Element of NAT such that
A1: [n,m] in Indices G and
A2: f /. i = G * n,m by Def11;
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_1:def 5;
hence n in dom G by A1, ZFMISC_1:106; :: thesis: f /. i in rng (Line G,n)
A4: m in Seg (width G) by A1, A3, ZFMISC_1:106;
len (Line G,n) = width G by MATRIX_1:def 8;
then A5: m in dom (Line G,n) by A4, FINSEQ_1:def 3;
(Line G,n) . m = f /. i by A2, A4, MATRIX_1:def 8;
hence f /. i in rng (Line G,n) by A5, FUNCT_1:def 5; :: thesis: verum