for F being RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of F
for seq being Real_Sequence st h1 is total & h2 is total holds
( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )