for D being non empty set
for d being Element of D
for f being FinSequence of PFuncs (D,REAL) st len f <> 0 holds
( d is_common_for_dom f iff d in dom (Sum f) )