theorem EXTh12: :: LOPBAN10:23

for G being RealNormSpace-Sequence
for p, q, r being Point of (product G) holds
( p + q = r iff for i being Element of dom G holds r . i = (p . i) + (q . i) )