for G being RealNormSpace-Sequence
for i being Element of dom G
for x being Point of (product G)
for a being Real holds (proj i) . (a * x) = a * ((proj i) . x)