reconsider mm = m as Element of INT by INT_1:def 2;
X --> m is {mm} -valued ;
hence for b₁ being Function st b₁ = X --> m holds
b₁ is INT -valued ; :: thesis: verum