let V, C be set ; for a being finite Element of PFuncs (V,C) holds {a} in SubstitutionSet (V,C)
let a be finite Element of PFuncs (V,C); {a} in SubstitutionSet (V,C)
A1:
for s, t being Element of PFuncs (V,C) st s in {a} & t in {a} & s c= t holds
s = t
for u being set st u in {a} holds
u is finite
;
then
{.a.} in { A where A is Element of Fin (PFuncs (V,C)) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs (V,C) st s in A & t in A & s c= t holds
s = t ) ) }
by A1;
hence
{a} in SubstitutionSet (V,C)
by SUBSTLAT:def 1; verum