let R be Relation; :: thesis: ( R is real-functions-valued implies R is ext-real-functions-valued )
assume A4: rng R is real-functions-membered ; :: according to VALUED_2:def 22 :: thesis: R is ext-real-functions-valued
let y be set ; :: according to VALUED_2:def 3,VALUED_2:def 21 :: thesis: ( y in rng R implies y is ext-real-valued Function )
thus ( y in rng R implies y is ext-real-valued Function ) by A4; :: thesis: verum