let X be Relation; :: thesis: ( X is empty implies X is natural-functions-valued )
assume A1: X is empty ; :: thesis: X is natural-functions-valued
let x be set ; :: according to VALUED_2:def 7,VALUED_2:def 25 :: thesis: ( x in rng X implies x is natural-valued Function )
thus ( x in rng X implies x is natural-valued Function ) by A1; :: thesis: verum