theorem Th7: :: PDIFF_7:7

for m, i being Nat
for x being Point of (REAL-NS m)
for p being Point of (REAL-NS 1) holds
( ((reproj (i,x)) . p) - x = (reproj (i,(0. (REAL-NS m)))) . (p - ((Proj (i,m)) . x)) & x - ((reproj (i,x)) . p) = (reproj (i,(0. (REAL-NS m)))) . (((Proj (i,m)) . x) - p) )