theorem Th20: :: PDIFF_7:20

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