let V be set ; :: thesis: for C being finite set
for a being Element of PFuncs V,C st a is finite holds
(Atom V,C) . a = {a}
let C be finite set ; :: thesis: for a being Element of PFuncs V,C st a is finite holds
(Atom V,C) . a = {a}
let a be Element of PFuncs V,C; :: thesis: ( a is finite implies (Atom V,C) . a = {a} )
assume A1: a is finite ; :: thesis: (Atom V,C) . a = {a}
{a} in SubstitutionSet V,C

proof

A2: for u being set st u in {a} holds
u is finite by A1, TARSKI:def 1;
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 ( s in {a} & t in {a} & s c= t ) ; :: thesis: s = t
then ( s = a & t = a ) by TARSKI:def 1;
hence s = t ; :: thesis: verum

end;

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 A2;
hence {a} in SubstitutionSet V,C by SUBSTLAT:def 1; :: thesis: verum

end;

then {a} = mi {.a.} by SUBSTLAT:11
.= (Atom V,C) . a by Def8 ;
hence (Atom V,C) . a = {a} ; :: thesis: verum