theorem Th16: :: MFOLD_2:16

for n, k being Nat
for p1, p2 being Point of (TOP-REAL n) st k in Seg n holds
(p1 + p2) . k = (p1 . k) + (p2 . k)