theorem :: ALTCAT_2:2

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