let V, C be set ; :: thesis: ( V is finite & C is finite implies PFuncs V,C is finite )
assume X: ( V is finite & C is finite ) ; :: thesis: PFuncs V,C is finite
PFuncs V,C c= bool [:V,C:] by Th4;
hence PFuncs V,C is finite by X; :: thesis: verum