theorem :: FUNCT_2:130

for A being set holds {} is Function of A,{} by Def1, RELSET_1:12;