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