thus f - x is Function of X,INT ; :: thesis: verum