theorem :: GOBRD13:8

for f being FinSequence of (TOP-REAL 2)
for G being Matrix of (TOP-REAL 2) st f is_sequence_on G holds
rng f c= Values G