theorem Th15: :: TOPREALC:15
for x being object
for n being Nat
for r being Real
for f1 being b2 -element real-valued FinSequence holds mlt (f1,((0.REAL n) +* (x,r))) = (0.REAL n) +* (x,((f1 . x) * r))