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