theorem Th6: :: JORDAN9:6

for G being Matrix of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Nat st 1 <= k & k <= len f holds
f /. k in Values G