reconsider h = {} as PartFunc of X,Y by RELSET_1:12;
take {h} ; :: thesis: for x being Element of {h} holds x is PartFunc of X,Y
thus for x being Element of {h} holds x is PartFunc of X,Y by TARSKI:def 1; :: thesis: verum