let X1, X2 be set ; :: thesis: for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds <-> (f1 <++> f2) = (<-> f1) <++> (<-> f2)
let Y1, Y2 be complex-functions-membered set ; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds <-> (f1 <++> f2) = (<-> f1) <++> (<-> f2)
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds <-> (f1 <++> f2) = (<-> f1) <++> (<-> f2)
let f2 be PartFunc of X2,Y2; :: thesis: <-> (f1 <++> f2) = (<-> f1) <++> (<-> f2)
set f3 = f1 <++> f2;
set f4 = <-> f1;
set f5 = <-> f2;
A1: dom (f1 <++> f2) = (dom f1) /\ (dom f2) by Def45;
A2: dom (<-> f2) = dom f2 by Def33;
A3: dom (<-> (f1 <++> f2)) = dom (f1 <++> f2) by Def33;
A4: dom (<-> f1) = dom f1 by Def33;
hence A5: dom (<-> (f1 <++> f2)) = dom ((<-> f1) <++> (<-> f2)) by A1, A2, A3, Def45; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (<-> (f1 <++> f2)) or (<-> (f1 <++> f2)) . b₁ = ((<-> f1) <++> (<-> f2)) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (<-> (f1 <++> f2)) or (<-> (f1 <++> f2)) . x = ((<-> f1) <++> (<-> f2)) . x )
assume A6: x in dom (<-> (f1 <++> f2)) ; :: thesis: (<-> (f1 <++> f2)) . x = ((<-> f1) <++> (<-> f2)) . x
then A7: x in dom (<-> f1) by A1, A4, A3, XBOOLE_0:def 4;
A8: x in dom (<-> f2) by A1, A2, A3, A6, XBOOLE_0:def 4;
thus (<-> (f1 <++> f2)) . x = - ((f1 <++> f2) . x) by A6, Def33
.= - ((f1 . x) + (f2 . x)) by A3, A6, Def45
.= (- (f1 . x)) - (f2 . x) by Th17
.= ((<-> f1) . x) + (- (f2 . x)) by A7, Def33
.= ((<-> f1) . x) + ((<-> f2) . x) by A8, Def33
.= ((<-> f1) <++> (<-> f2)) . x by A5, A6, Def45 ; :: thesis: verum