theorem Th15: :: NDIFF_5:15

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) )