theorem Th17: :: PDIFF_7:17

for m being non zero Nat
for x being Element of REAL
for i being Nat st 1 <= i & i <= m & x <> 0 holds
(reproj (i,(0* m))) . x <> 0* m