set h = f <##> g;
A1:
dom (f <##> g) = (dom f) /\ (dom g)
by Def47;
rng (f <##> g) c= R_PFuncs ((DOMS Y1) /\ (DOMS Y2))
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (f <##> g) or y in R_PFuncs ((DOMS Y1) /\ (DOMS Y2)) )
assume
y in rng (f <##> g)
;
y in R_PFuncs ((DOMS Y1) /\ (DOMS Y2))
then consider x being
object such that A2:
x in dom (f <##> g)
and A3:
(f <##> g) . x = y
by FUNCT_1:def 3;
reconsider y =
y as
Function by A3;
A4:
(f <##> g) . x = (f . x) (#) (g . x)
by A2, Def47;
A5:
rng y c= REAL
by A3, A4, XREAL_0:def 1;
x in dom g
by A1, A2, XBOOLE_0:def 4;
then
g . x in Y2
by PARTFUN1:4;
then
dom (g . x) in { (dom m) where m is Element of Y2 : verum }
;
then A6:
dom (g . x) c= DOMS Y2
by ZFMISC_1:74;
x in dom f
by A1, A2, XBOOLE_0:def 4;
then
f . x in Y1
by PARTFUN1:4;
then
dom (f . x) in { (dom m) where m is Element of Y1 : verum }
;
then A7:
dom (f . x) c= DOMS Y1
by ZFMISC_1:74;
dom y = (dom (f . x)) /\ (dom (g . x))
by A3, A4, VALUED_1:def 4;
then
y is
PartFunc of
((DOMS Y1) /\ (DOMS Y2)),
REAL
by A7, A6, A5, RELSET_1:4, XBOOLE_1:27;
hence
y in R_PFuncs ((DOMS Y1) /\ (DOMS Y2))
by Def12;
verum
end;
hence
f <##> g is PartFunc of (X1 /\ X2),(R_PFuncs ((DOMS Y1) /\ (DOMS Y2)))
by A1, RELSET_1:4; verum