let G be Matrix of (TOP-REAL 2); :: thesis: 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
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for k being Nat st 1 <= k & k <= len f holds
f /. k in Values G )
assume A1: f is_sequence_on G ; :: thesis: for k being Nat st 1 <= k & k <= len f holds
f /. k in Values G
let k be Nat; :: thesis: ( 1 <= k & k <= len f implies f /. k in Values G )
assume A2: ( 1 <= k & k <= len f ) ; :: thesis: f /. k in Values G
A3: k in dom f by A2, FINSEQ_3:25;
then f /. k = f . k by PARTFUN1:def 6;
then A4: f /. k in rng f by A3, FUNCT_1:def 3;
rng f c= Values G by A1, GOBRD13:8;
hence f /. k in Values G by A4; :: thesis: verum