set h = f <-> g;
A1: dom (f <-> g) = (dom f) /\ (dom g) by Th61;
rng (f <-> g) c= C_PFuncs (DOMS Y)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f <-> g) or y in C_PFuncs (DOMS Y) )
assume y in rng (f <-> g) ; :: thesis: y in C_PFuncs (DOMS Y)
then consider x being set such that
A2: x in dom (f <-> g) and
A3: (f <-> g) . x = y by FUNCT_1:def 3;
B4: (f <-> g) . x = (f . x) - (g . x) by A2, Th62;
then reconsider y = y as Function by A3;
A4: 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 A3, B4, XCMPLX_0:def 2; :: thesis: verum

end;

x in dom f by A1, A2, XBOOLE_0:def 4;
then f . x in Y by PARTFUN1:4;
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:74;
(f <-> g) . x = (f . x) - (g . x) by A2, Th62;
then dom y = dom (f . x) by A3, VALUED_1:def 2;
then y is PartFunc of (DOMS Y),COMPLEX by A5, A4, RELSET_1:4;
hence y in C_PFuncs (DOMS Y) by Def8; :: thesis: verum

end;

hence f <-> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) by A1, RELSET_1:4, XBOOLE_1:27; :: thesis: verum