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