let V, C be set ; :: thesis: {{} } in SubstitutionSet V,C
{} is PartFunc of V,C by RELSET_1:25;
then {} in PFuncs V,C by PARTFUN1:119;
then {{} } c= PFuncs V,C by ZFMISC_1:37;
then A1: {{} } in Fin (PFuncs V,C) by FINSUB_1:def 5;
A2: for u being set st u in {{} } holds
u is finite by TARSKI:def 1;
for s, t being Element of PFuncs V,C st s in {{} } & t in {{} } & s c= t holds
s = t

proof

let s, t be Element of PFuncs V,C; :: thesis: ( s in {{} } & t in {{} } & s c= t implies s = t )
assume ( s in {{} } & t in {{} } & s c= t ) ; :: thesis: s = t
then ( s = {} & t = {} ) by TARSKI:def 1;
hence s = t ; :: thesis: verum

end;

hence {{} } in SubstitutionSet V,C by A1, A2; :: thesis: verum