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

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