theorem :: RFUNCT_3:27

for D, C being non empty set
for f being FinSequence of PFuncs (D,C)
for d being Element of D
for n being Nat st d is_common_for_dom f holds
d is_common_for_dom f /^ n