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