theorem :: FUNCT_1:104

for f being Function holds {} is f -compatible ;