let X1, X2, X3, X4, X5 be set ; :: thesis: for Y1, Y2, Y3, Y4, Y5 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let Y1, Y2, Y3, Y4, Y5 be complex-functions-membered set ; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2
for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let f2 be PartFunc of X2,Y2; :: thesis: for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let f3 be PartFunc of X3,Y3; :: thesis: for f4 being PartFunc of X4,Y4
for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let f4 be PartFunc of X4,Y4; :: thesis: for f5 being PartFunc of X5,Y5 st f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 holds
<-> f3 = f4 <++> f5
let f5 be PartFunc of X5,Y5; :: thesis: ( f3 = f1 <++> f2 & f4 = <-> f1 & f5 = <-> f2 implies <-> f3 = f4 <++> f5 )
assume that
a1: f3 = f1 <++> f2 and
a2: f4 = <-> f1 and
a3: f5 = <-> f2 ; :: thesis: <-> f3 = f4 <++> f5
a4: dom (f1 <++> f2) = (dom f1) /\ (dom f2) by Def44;
a5: dom (<-> f1) = dom f1 by Def32;
a6: dom (<-> f2) = dom f2 by Def32;
a7: dom (<-> f3) = dom f3 by Def32;
hence A1: dom (<-> f3) = dom (f4 <++> f5) by a1, a2, a3, a4, a5, a6, Def44; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (<-> f3) or (<-> f3) . b₁ = (f4 <++> f5) . b₁ )
let x be set ; :: thesis: ( not x in dom (<-> f3) or (<-> f3) . x = (f4 <++> f5) . x )
assume A2: x in dom (<-> f3) ; :: thesis: (<-> f3) . x = (f4 <++> f5) . x
then a8: x in dom f4 by a1, a2, a4, a5, a7, XBOOLE_0:def 4;
a9: x in dom f5 by a1, a3, a4, a6, a7, A2, XBOOLE_0:def 4;
thus (<-> f3) . x = - (f3 . x) by A2, Def32
.= - ((f1 . x) + (f2 . x)) by a1, a7, A2, Def44
.= (- (f1 . x)) - (f2 . x) by Th13a
.= (f4 . x) + (- (f2 . x)) by a2, a8, Def32
.= (f4 . x) + (f5 . x) by a3, a9, Def32
.= (f4 <++> f5) . x by A2, A1, Def44 ; :: thesis: verum