set h = abs f;
a2: dom (abs f) = dom f by Def35;
rng (abs f) c= C_PFuncs (DOMS Y)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (abs f) or y in C_PFuncs (DOMS Y) )
assume y in rng (abs f) ; :: thesis: y in C_PFuncs (DOMS Y)
then consider x being set such that
a3: x in dom (abs f) and
a4: (abs f) . x = y by FUNCT_1:def 5;
a7: (abs f) . x = abs (f . x) by a3, Def35;
then reconsider y = y as Function by a4;
b2: dom y = dom (f . x) by a4, a7, VALUED_1:def 11;
f . x in Y by a2, a3, PARTFUN1:27;
then dom (f . x) in { (dom m) where m is Element of Y : verum } ;
then a5: dom (f . x) c= DOMS Y by ZFMISC_1:92;
rng y c= COMPLEX

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng y or b in COMPLEX )
thus ( not b in rng y or b in COMPLEX ) by a4, a7, XCMPLX_0:def 2; :: thesis: verum

end;

then y is PartFunc of (DOMS Y),COMPLEX by a5, b2, RELSET_1:11;
hence y in C_PFuncs (DOMS Y) by Def7; :: thesis: verum

end;

hence abs f is PartFunc of X,(C_PFuncs (DOMS Y)) by a2, RELSET_1:11; :: thesis: verum