let X be set ; for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g
let Y be complex-functions-membered set ; for f being PartFunc of X,Y
for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g
let f be PartFunc of X,Y; for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g
let g be complex-valued Function; <-> (f <-> g) = (<-> f) <+> g
set f1 = f <-> g;
set f2 = <-> f;
A1:
dom (<-> (f <-> g)) = dom (f <-> g)
by Def33;
A2:
( dom (f <-> g) = (dom f) /\ (dom g) & dom (<-> f) = dom f )
by Def33, Th61;
hence A3:
dom (<-> (f <-> g)) = dom ((<-> f) <+> g)
by A1, Def41; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (<-> (f <-> g)) or (<-> (f <-> g)) . b1 = ((<-> f) <+> g) . b1 )
let x be object ; ( not x in dom (<-> (f <-> g)) or (<-> (f <-> g)) . x = ((<-> f) <+> g) . x )
assume A4:
x in dom (<-> (f <-> g))
; (<-> (f <-> g)) . x = ((<-> f) <+> g) . x
then A5:
x in dom (<-> f)
by A1, A2, XBOOLE_0:def 4;
thus (<-> (f <-> g)) . x =
- ((f <-> g) . x)
by A4, Def33
.=
- ((f . x) - (g . x))
by A1, A4, Th62
.=
(- (f . x)) + (g . x)
by Th11
.=
((<-> f) . x) + (g . x)
by A5, Def33
.=
((<-> f) <+> g) . x
by A3, A4, Def41
; verum