theorem :: JORDAN2B:5

for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 + p2) /. i = (p1 /. i) + (p2 /. i)