theorem Th19: :: PDIFF_7:19

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