x (#) f is Function of X,INT ;
hence f * x is Function of X,INT ; :: thesis: verum