a is integer ;
then reconsider a = a as Element of INT ;
thus n |-> a is INT -valued ; :: thesis: verum