theorem Th25: :: NDIFF_1:25

for S, T being RealNormSpace
for h1, h2 being PartFunc of S,T
for seq being sequence of S st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )