theorem Th25: :: NCFCONT1:25

for CNS being ComplexNormSpace
for RNS being RealNormSpace
for h1, h2 being PartFunc of RNS,CNS
for seq being sequence of RNS st rng seq c= (dom h1) /\ (dom h2) holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )