let X be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g

let g be complex-valued Function; :: thesis: <-> (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; :: according to FUNCT_1:def 11 :: thesis: for b_{1} being object holds

( not b_{1} in dom (<-> (f <-> g)) or (<-> (f <-> g)) . b_{1} = ((<-> f) <+> g) . b_{1} )

let x be object ; :: thesis: ( not x in dom (<-> (f <-> g)) or (<-> (f <-> g)) . x = ((<-> f) <+> g) . x )

assume A4: x in dom (<-> (f <-> g)) ; :: thesis: (<-> (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 ; :: thesis: verum

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 ; :: thesis: 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; :: thesis: for g being complex-valued Function holds <-> (f <-> g) = (<-> f) <+> g

let g be complex-valued Function; :: thesis: <-> (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; :: according to FUNCT_1:def 11 :: thesis: for b

( not b

let x be object ; :: thesis: ( not x in dom (<-> (f <-> g)) or (<-> (f <-> g)) . x = ((<-> f) <+> g) . x )

assume A4: x in dom (<-> (f <-> g)) ; :: thesis: (<-> (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 ; :: thesis: verum