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

proof

let e be object ; :: 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 object such that
A2: u in dom ||.f.|| and
A3: e = ||.f.|| . u by FUNCT_1:def 3;
e = ||.(f /. u).|| by A2, A3, Def2;
hence e in REAL ; :: thesis: verum

end;

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