set h = f <-> g;
A1:
dom (f <-> g) = (dom f) /\ (dom g)
by Th61;
rng (f <-> g) c= C_PFuncs (DOMS Y)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (f <-> g) or y in C_PFuncs (DOMS Y) )
assume
y in rng (f <-> g)
;
y in C_PFuncs (DOMS Y)
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 A2, Th62;
then reconsider y =
y as
Function by A3;
A5:
rng y c= COMPLEX
by A3, A4, XCMPLX_0:def 2;
x in dom f
by A1, A2, XBOOLE_0:def 4;
then
f . x in Y
by PARTFUN1:4;
then
dom (f . x) in { (dom m) where m is Element of Y : verum }
;
then A6:
dom (f . x) c= DOMS Y
by ZFMISC_1:74;
(f <-> g) . x = (f . x) - (g . x)
by A2, Th62;
then
dom y = dom (f . x)
by A3, VALUED_1:def 2;
then
y is
PartFunc of
(DOMS Y),
COMPLEX
by A6, A5, RELSET_1:4;
hence
y in C_PFuncs (DOMS Y)
by Def8;
verum
end;
hence
f <-> g is PartFunc of (X /\ (dom g)),(C_PFuncs (DOMS Y))
by A1, RELSET_1:4, XBOOLE_1:27; verum