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