let f be Function; :: thesis: ( f is X -valued implies f is Function-yielding )
assume f is X -valued ; :: thesis: f is Function-yielding
then reconsider g = f as X -valued Function ;

now

let x be set ; :: thesis: ( x in dom g implies f . x is Function )
assume x in dom g ; :: thesis: f . x is Function
then g . x in X by FUNCT_1:102;
hence f . x is Function ; :: thesis: verum

end;

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