theorem :: PRE_POLY:14

for V, C being non empty set ex f being Element of PFuncs (V,C) st f <> {}