let X be set ; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <+> g) <-> h = f <+> (g - h)
let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for g, h being complex-valued Function holds (f <+> g) <-> h = f <+> (g - h)
let f be PartFunc of X,Y; :: thesis: for g, h being complex-valued Function holds (f <+> g) <-> h = f <+> (g - h)
let g, h be complex-valued Function; :: thesis: (f <+> g) <-> h = f <+> (g - h)
set f1 = f <+> g;
A2:
dom (f <+> g) = (dom f) /\ (dom g)
by Def40;
A3:
dom ((f <+> g) <-> h) = (dom (f <+> g)) /\ (dom h)
by Th35;
A4:
dom (f <+> (g - h)) = (dom f) /\ (dom (g - h))
by Def40;
dom (g - h) = (dom g) /\ (dom h)
by VALUED_1:12;
hence A5:
dom ((f <+> g) <-> h) = dom (f <+> (g - h))
by A2, A3, A4, XBOOLE_1:16; :: according to FUNCT_1:def 17 :: thesis: for b1 being set holds
( not b1 in dom ((f <+> g) <-> h) or ((f <+> g) <-> h) . b1 = (f <+> (g - h)) . b1 )
let x be set ; :: thesis: ( not x in dom ((f <+> g) <-> h) or ((f <+> g) <-> h) . x = (f <+> (g - h)) . x )
assume A6:
x in dom ((f <+> g) <-> h)
; :: thesis: ((f <+> g) <-> h) . x = (f <+> (g - h)) . x
then A7:
x in dom (f <+> g)
by A3, XBOOLE_0:def 4;
A8:
x in dom (g - h)
by A6, A5, XBOOLE_0:def 4;
thus ((f <+> g) <-> h) . x =
((f <+> g) . x) - (h . x)
by A6, Th36
.=
((f . x) + (g . x)) - (h . x)
by A7, Def40
.=
(f . x) + ((g . x) - (h . x))
by Th9
.=
(f . x) + ((g - h) . x)
by A8, VALUED_1:13
.=
(f <+> (g - h)) . x
by A6, A5, Def40
; :: thesis: verum