theorem Th31: :: NCFCONT1:31

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