let C be set ; :: thesis: for f being C -defined total Function holds f is Function of C,(rng f)
let f be C -defined total Function; :: thesis: f is Function of C,(rng f)
dom f = C by PARTFUN1:def 2;
hence f is Function of C,(rng f) by FUNCT_2:1; :: thesis: verum