theorem Th30: :: NCFCONT1:30

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