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