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 set ; :: 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:4;
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) by A1, A2, GOBOARD1:def 11;
then y in { (G * i,j) where i, j is Element of NAT : [i,j] in Indices G } by A3;
hence y in Values G by Th7; :: thesis: verum