for X, Y being set
for r being Real
for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds
( r in X /\ (dom h1) & r in Y /\ (dom h2) )