theorem :: HEYTING3:8

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