theorem :: HEYTING2:16

for V being set
for C being finite set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
A =>> A = {{}}