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