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