dom ||.f.|| = dom f by Def1;
then A: dom ||.f.|| c= C by RELAT_1:def 18;
rng ||.f.|| c= REAL

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in rng ||.f.|| or e in REAL )
assume e in rng ||.f.|| ; :: thesis: e in REAL
then consider u being set such that
W1: u in dom ||.f.|| and
W2: e = ||.f.|| . u by FUNCT_1:def 5;
e = ||.(f /. u).|| by W1, W2, Def1;
hence e in REAL ; :: thesis: verum

end;

hence ||.f.|| is PartFunc of C,REAL by A, RELSET_1:11; :: thesis: verum