theorem Th13: :: NFCONT_1:13

for S, T being RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)