for D being non empty set
for H1, H2 being Functional_Sequence of D,REAL
for X being set st X common_on_dom H1 & X common_on_dom H2 holds
( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 )