theorem :: HEYTING2:8

for C being finite set
for A being Element of Fin (PFuncs ({},C)) holds Involved A = {} by Th6, XBOOLE_1:3;