for i being Nat
for c being Complex
for R being b₁ -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R