theorem Th4: :: NFCONT_3:4

for S being RealNormSpace
for h being PartFunc of REAL, the carrier of S
for seq being Real_Sequence
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)