let V be set ; :: thesis: for C being finite set
for a being finite Element of PFuncs V,C holds a in (Atom V,C) . a
let C be finite set ; :: thesis: for a being finite Element of PFuncs V,C holds a in (Atom V,C) . a
let a be finite Element of PFuncs V,C; :: thesis: a in (Atom V,C) . a
(Atom V,C) . a = {a} by Lm7;
hence a in (Atom V,C) . a by TARSKI:def 1; :: thesis: verum