let f be PartFunc of X,Y; :: thesis: f is integer-functions-valued
let x be set ; :: according to VALUED_2:def 30 :: thesis: ( x in dom f implies f . x is integer-valued Function )
thus ( x in dom f implies f . x is integer-valued Function ) ; :: thesis: verum