let C, D be set ; :: thesis: for f being C -defined total Function holds
( f is Function of C,D iff f is D -valued )
let f be C -defined total Function; :: thesis: ( f is Function of C,D iff f is D -valued )
reconsider f1 = f as Function of C,(rng f) by T2103;
( f1 is D -valued implies f is Function of (dom f),D ) by N2103;
hence ( f is Function of C,D iff f is D -valued ) by PARTFUN1:def 2; :: thesis: verum