set h = f <--> g;
A1: dom (f <--> g) = (dom f) /\ (dom g) by Def46;
rng (f <--> g) c= C_PFuncs ((DOMS Y1) /\ (DOMS Y2))
proof
let y be object ; :: 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 object such that
A2: x in dom (f <--> g) and
A3: (f <--> g) . x = y by FUNCT_1:def 3;
A4: (f <--> g) . x = (f . x) - (g . x) by ;
then reconsider y = y as Function by A3;
A5: rng y c= COMPLEX by ;
x in dom g by ;
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 ;
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 ;
then y is PartFunc of ((DOMS Y1) /\ (DOMS Y2)),COMPLEX by ;
hence y in C_PFuncs ((DOMS Y1) /\ (DOMS Y2)) by Def8; :: thesis: verum
end;
hence f <--> g is PartFunc of (X1 /\ X2),(C_PFuncs ((DOMS Y1) /\ (DOMS Y2))) by ; :: thesis: verum