i in INT by INT_1:def 2;
hence (Funcs (X,INT)) --> i is INT-Expression of X by FUNCOP_1:45; :: thesis: verum