let V, C be set ; :: thesis: {{} } in SubstitutionSet V,C
A1: 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 that
A2: s in {{} } and
A3: t in {{} } and
s c= t ; :: thesis: s = t
s = {} by A2, TARSKI:def 1;
hence s = t by A3, TARSKI:def 1; :: thesis: verum

end;

{} 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 A4: {{} } in Fin (PFuncs V,C) by FINSUB_1:def 5;
for u being set st u in {{} } holds
u is finite by TARSKI:def 1;
hence {{} } in SubstitutionSet V,C by A4, A1; :: thesis: verum