theorem Th14: :: NFCONT_1:14

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