let f be FinSequence of (TOP-REAL 2); :: thesis: for G being Matrix of (TOP-REAL 2) st f is_sequence_on G holds
rng f c= Values G
let G be Matrix of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies rng f c= Values G )
assume A1: f is_sequence_on G ; :: thesis: rng f c= Values G
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Values G )
assume y in rng f ; :: thesis: y in Values G
then consider n being Element of NAT such that
A2: n in dom f and
A3: f /. n = y by PARTFUN2:2;
ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) by A1, A2, GOBOARD1:def 9;
then y in { (G * (i,j)) where i, j is Nat : [i,j] in Indices G } by A3;
hence y in Values G by MATRIX_0:39; :: thesis: verum