for f, g being Function holds ~ (g * f) = g * (~ f)