theorem :: ORDEQ_01:37

for n being non zero Element of NAT
for i being Nat
for y1, y2 being Point of (REAL-NS n) holds (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2)