set h = f <--> g;
a2: dom (f <--> g) = (dom f) /\ (dom g) by Def45;
rng (f <--> g) c= C_PFuncs ((DOMS Y1) /\ (DOMS Y2))

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f <--> g) or y in C_PFuncs ((DOMS Y1) /\ (DOMS Y2)) )
assume y in rng (f <--> g) ; :: thesis: y in C_PFuncs ((DOMS Y1) /\ (DOMS Y2))
then consider x being set such that
a3: x in dom (f <--> g) and
a4: (f <--> g) . x = y by FUNCT_1:def 5;
a7: (f <--> g) . x = (f . x) - (g . x) by a3, Def45;
then reconsider y = y as Function by a4;
b2: dom y = (dom (f . x)) /\ (dom (g . x)) by a4, a7, VALUED_1:12;
( x in dom f & x in dom g ) by a2, a3, XBOOLE_0:def 4;
then ( f . x in Y1 & g . x in Y2 ) by PARTFUN1:27;
then ( dom (f . x) in { (dom m) where m is Element of Y1 : verum } & dom (g . x) in { (dom m) where m is Element of Y2 : verum } ) ;
then a5: ( dom (f . x) c= DOMS Y1 & dom (g . x) c= DOMS Y2 ) 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 Y1) /\ (DOMS Y2)),COMPLEX by a5, b2, XBOOLE_1:27, RELSET_1:11;
hence y in C_PFuncs ((DOMS Y1) /\ (DOMS Y2)) by Def7; :: thesis: verum

end;

hence f <--> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) by a2, XBOOLE_1:27, RELSET_1:11; :: thesis: verum