let D be set ; :: thesis: for f being Function holds
( f is D -valued iff f is Function of (dom f),D )
let f be Function; :: thesis: ( f is D -valued iff f is Function of (dom f),D )
thus ( f is D -valued implies f is Function of (dom f),D ) :: thesis: ( f is Function of (dom f),D implies f is D -valued )

proof

assume f is D -valued ; :: thesis: f is Function of (dom f),D
then rng f c= D by RELAT_1:def 19;
hence f is Function of (dom f),D by FUNCT_2:2; :: thesis: verum

end;

thus ( f is Function of (dom f),D implies f is D -valued ) ; :: thesis: verum