for V being set
for C being finite set
for a being Element of PFuncs (V,C) st a is finite holds
for c being set st c in (Atom (V,C)) . a holds
c = a