theorem Th5: :: NFCONT_3:5

for S being RealNormSpace
for h being PartFunc of REAL, the carrier of S
for seq being Real_Sequence st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )