theorem :: FUNCT_4:20

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