for D being non empty set
for Y being RealNormSpace
for H1, H2 being Functional_Sequence of D, the carrier of Y
for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds
( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x )