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