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