let V, C be set ; :: thesis: {} in SubstitutionSet (V,C)
{} c= PFuncs (V,C) ;
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