theorem Th13: :: NDIFF_5:13

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