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