let R be Relation; :: thesis: ( R is natural-functions-valued implies R is integer-functions-valued )
assume A1: rng R is natural-functions-membered ; :: according to VALUED_2:def 25 :: thesis: R is integer-functions-valued
let y be set ; :: according to VALUED_2:def 6,VALUED_2:def 24 :: thesis: ( y in rng R implies y is integer-valued Function )
thus ( y in rng R implies y is integer-valued Function ) by A1; :: thesis: verum