theorem :: SUBSTLAT:9

for V, C being set
for A being Element of Fin (PFuncs (V,C)) st A = {} holds
mi A = {} by Th8, XBOOLE_1:3;