:: deftheorem Def26 defines PFuncsDomHQN MARGREL1:def 26 :
for D, b₂ being non empty set holds
( b₂ is PFuncsDomHQN of D iff for x being Element of b₂ holds x is non empty homogeneous quasi_total PartFunc of (D *),D );