theorem Th6: :: PDIFF_7:6

for m, i being Nat
for x being Element of REAL m
for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )