let f be Function; :: thesis: ( f is Function-yielding implies f is Relation-yielding )
assume Z: f is Function-yielding ; :: thesis: f is Relation-yielding
let x be set ; :: according to FUNCOP_1:def 11 :: thesis: ( x in dom f implies f . x is Relation )
thus ( x in dom f implies f . x is Relation ) by Z; :: thesis: verum