theorem Th18: :: PDIFF_7:18

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