let V, C be set ; :: thesis: for a being finite Element of PFuncs V,C holds {a} in SubstitutionSet V,C
let a be finite Element of PFuncs V,C; :: thesis: {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

proof

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

end;

for u being set st u in {a} holds
u is finite by TARSKI:def 1;
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; :: thesis: verum