set h = f <#> g;
a2: dom (f <#> g) = (dom f) /\ (dom g) by Def42;
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
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, Def42;
then reconsider y = y as Function by a4;
b2: dom y = dom (f . x) by a4, a7, VALUED_1:def 5;
( x in dom f & x in dom g ) by a2, a3, XBOOLE_0:def 4;
then f . x in Y by 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 f <#> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y)) by a2, XBOOLE_1:27, RELSET_1:11; :: thesis: verum