theorem Th26: :: NCFCONT1:26

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