theorem Th15: :: PDIFF_7:15

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