let V, C be set ; :: thesis: ( V is finite & C is finite implies PFuncs (V,C) is finite )
assume that
A1: V is finite and
A2: C is finite ; :: thesis: PFuncs (V,C) is finite
PFuncs (V,C) c= bool [:V,C:] by Th15;
hence PFuncs (V,C) is finite by A1, A2; :: thesis: verum