theorem :: REAL_NS2:20

for n being Nat
for F being FinSequence of (REAL-NS n)
for fr being Function of (REAL-NS n),REAL
for Fv being FinSequence of (n -VectSp_over F_Real)
for fv being Function of (n -VectSp_over F_Real),F_Real st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv