theorem Th27: :: NCFCONT1:27

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