theorem Th12: :: NDIFF_5:12

for G being RealNormSpace-Sequence
for p, q being Point of (product G)
for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds
( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )