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:12;
then {} in PFuncs (V,C) by PARTFUN1:45;
then {{}} c= PFuncs (V,C) by ZFMISC_1:31;
then A4: {{}} in Fin (PFuncs (V,C)) by FINSUB_1:def 5;
for u being set st u in {{}} holds
u is finite ;
hence {{}} in SubstitutionSet (V,C) by A4, A1; :: thesis: verum