let i be Nat; :: thesis: for G being Go-board
for f being FinSequence of () 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 () 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 (); :: 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 ()):] by MATRIX_0:def 4;
hence n in dom G by ; :: thesis: f /. i in rng (Line (G,n))
A4: m in Seg () by ;
len (Line (G,n)) = width G by MATRIX_0:def 7;
then A5: m in dom (Line (G,n)) by ;
(Line (G,n)) . m = f /. i by ;
hence f /. i in rng (Line (G,n)) by ; :: thesis: verum