let V, C be set ; :: thesis: {} in SubstitutionSet V,C
{} c= PFuncs V,C by XBOOLE_1:2;
then A1: {} in Fin (PFuncs V,C) by FINSUB_1:def 5;
( ( for u being set st u in {} holds
u is finite ) & ( for s, t being Element of PFuncs V,C st s in {} & t in {} & s c= t holds
s = t ) ) ;
hence {} in SubstitutionSet V,C by A1; :: thesis: verum