theorem Th10: :: PDIFF_7:10

for m being non zero Nat
for x, a being Real
for i being Nat st 1 <= i & i <= m holds
(0* m) +* (i,(a * x)) = a * (Replace ((0* m),i,x))