for f being Function holds {} in sproduct f