for E being RealNormSpace
for a being Point of E
for f being Real_Sequence holds f (#) (NAT --> a) = f * a