theorem EXTh13: :: LOPBAN10:24

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