theorem :: FUNCT_4:21

for f being Function holds f +* {} = f ;