let x be object ; :: according to VALUED_2:def 6 :: thesis: ( x in Funcs (X,Y) implies x is INT -valued Function )
assume x in Funcs (X,Y) ; :: thesis: x is INT -valued Function
then consider f being Function such that
A1: x = f and
A2: ( dom f = X & rng f c= Y ) by FUNCT_2:def 2;
reconsider f = f as PartFunc of X,Y by A2, RELSET_1:4;
f is set ;
hence x is INT -valued Function by A1; :: thesis: verum