:: deftheorem defines is_common_for_dom RFUNCT_3:def 9 :
for D, C being non empty set
for f being FinSequence of PFuncs (D,C)
for d being Element of D holds
( d is_common_for_dom f iff for n being Nat st n in dom f holds
d in dom (f . n) );