thus ( f is Function-yielding implies rng f is functional ) :: thesis: ( rng f is functional implies f is Function-yielding )

proof

assume A1: f is Function-yielding ; :: thesis: rng f is functional
let o be object ; :: according to FUNCT_1:def 13 :: thesis: ( not o in rng f or o is set )
assume o in rng f ; :: thesis: o is set
then ex x being object st
( x in dom f & f . x = o ) by FUNCT_1:def 3;
hence o is set by A1; :: thesis: verum

end;

assume A2: rng f is functional ; :: thesis: f is Function-yielding

now :: thesis: for o being object st o in dom f holds
f . o is Function

let o be object ; :: thesis: ( o in dom f implies f . o is Function )
assume o in dom f ; :: thesis: f . o is Function
then f . o in rng f by FUNCT_1:def 3;
hence f . o is Function by A2; :: thesis: verum

end;

hence f is Function-yielding by FUNCOP_1:def 6; :: thesis: verum