for X being RealNormSpace-Sequence
for s being Point of (product X)
for a being FinSequence of REAL ex s1 being Point of (product X) st
for i being Element of dom X holds s1 . i = (a /. i) * (s . i)