let A be Element of SubstitutionSet (V,C); :: thesis: A is functional
A c= PFuncs (V,C) by FINSUB_1:def 5;
hence A is functional ; :: thesis: verum