theorem Th29: :: NCFCONT1:29

for CNS1, CNS2 being ComplexNormSpace
for h being PartFunc of CNS1,CNS2
for seq being sequence of CNS1 st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )