for n being non zero Element of NAT
for x, y being Point of (REAL-NS n)
for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)