set h = f <##> g;
a2: dom (f <##> g) = (dom f) /\ (dom g) by Def46;
rng (f <##> g) c= R_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 R_PFuncs ((DOMS Y1) /\ (DOMS Y2)) )
assume y in rng (f <##> g) ; :: thesis: y in R_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, Def46;
reconsider y = y as Function by a4;
b2: dom y = (dom (f . x)) /\ (dom (g . x)) by a4, a7, VALUED_1:def 4;
( 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= REAL

proof

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

end;

then y is PartFunc of ((DOMS Y1) /\ (DOMS Y2)),REAL by a5, b2, XBOOLE_1:27, RELSET_1:11;
hence y in R_PFuncs ((DOMS Y1) /\ (DOMS Y2)) by Def11; :: thesis: verum

end;

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