thus t1 + t2 is Function of X, INT ; :: thesis: verum