theorem Th13: :: PDIFF_7:13

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