theorem :: LOPBAN10:26

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