theorem Th2: :: NFCONT_3:2

for S being RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of S
for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )