theorem Th16: :: PDIFF_7:16

for m being non zero Nat
for x being Point of (REAL-NS 1)
for a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)