theorem Th14: :: PDIFF_7:14

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