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