set h = </> f;
A1: dom (</> f) = dom f by Def35;
rng (</> f) c= Q_PFuncs (DOMS Y)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (</> f) or y in Q_PFuncs (DOMS Y) )
assume y in rng (</> f) ; :: thesis: y in Q_PFuncs (DOMS Y)
then consider x being object such that
A2: x in dom (</> f) and
A3: (</> f) . x = y by FUNCT_1:def 3;
reconsider y = y as Function by A3;
A4: (</> f) . x = (f . x) " by A2, Def35;
A5: rng y c= RAT by A3, A4, RAT_1:def 2;
f . x in Y by A1, A2, PARTFUN1:4;
then dom (f . x) in { (dom m) where m is Element of Y : verum } ;
then A6: dom (f . x) c= DOMS Y by ZFMISC_1:74;
dom y = dom (f . x) by A3, A4, VALUED_1:def 7;
then y is PartFunc of (DOMS Y),RAT by A6, A5, RELSET_1:4;
hence y in Q_PFuncs (DOMS Y) by Def14; :: thesis: verum

end;

hence </> f is PartFunc of X,(Q_PFuncs (DOMS Y)) by A1, RELSET_1:4; :: thesis: verum