theorem :: TOPREALC:16

for x being object
for n being Nat
for r being Real
for f1 being b₂ -element real-valued FinSequence holds |(f1,((0.REAL n) +* (x,r)))| = (f1 . x) * r