theorem Th1: :: FUNCTOR0:1

for A being set holds {} is Function of A,{} by FUNCT_2:130;