reconsider a1 = a, b1 = b as Element of INT by INT_1:def 2;
<%a,b%> = ((0_. F_Real) +* (0,a1)) +* (1,b1) ;
hence <%a,b%> is INT -valued ; :: thesis: verum