for D being non empty set
for d being Element of D
for f being FinSequence of PFuncs (D,REAL) st d is_common_for_dom f holds
(Sum f) . d = Sum (f # d)