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