theorem Th8: :: MAZURULM:8

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