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