let X, X1, X2, X3, X4 be set ; :: thesis: for Y, Y1, Y2, Y3, Y4 being complex-functions-membered set
for f being PartFunc of X,Y
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 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
let Y, Y1, Y2, Y3, Y4 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
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 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
let f be PartFunc of X,Y; :: 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 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
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 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
let f2 be PartFunc of X2,Y2; :: thesis: for f3 being PartFunc of X3,Y3
for f4 being PartFunc of X4,Y4 st f3 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
let f3 be PartFunc of X3,Y3; :: thesis: for f4 being PartFunc of X4,Y4 st f3 = f <++> f1 & f4 = f1 <++> f2 holds
f3 <++> f2 = f <++> f4
let f4 be PartFunc of X4,Y4; :: thesis: ( f3 = f <++> f1 & f4 = f1 <++> f2 implies f3 <++> f2 = f <++> f4 )
assume that
A1: f3 = f <++> f1 and
A2: f4 = f1 <++> f2 ; :: thesis: f3 <++> f2 = f <++> f4
A3: dom f3 = (dom f) /\ (dom f1) by A1, Def44;
A4: dom f4 = (dom f1) /\ (dom f2) by A2, Def44;
A5: dom (f3 <++> f2) = (dom f3) /\ (dom f2) by Def44;
A6: dom (f <++> f4) = (dom f) /\ (dom f4) by Def44;
hence A7: dom (f3 <++> f2) = dom (f <++> f4) by A3, A5, A4, XBOOLE_1:16; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (f3 <++> f2) or (f3 <++> f2) . b₁ = (f <++> f4) . b₁ )
let x be set ; :: thesis: ( not x in dom (f3 <++> f2) or (f3 <++> f2) . x = (f <++> f4) . x )
assume A8: x in dom (f3 <++> f2) ; :: thesis: (f3 <++> f2) . x = (f <++> f4) . x
then A9: x in dom f3 by A5, XBOOLE_0:def 4;
A10: x in dom f4 by A6, A8, A7, XBOOLE_0:def 4;
thus (f3 <++> f2) . x = (f3 . x) + (f2 . x) by A8, Def44
.= ((f . x) + (f1 . x)) + (f2 . x) by A1, A9, Def44
.= (f . x) + ((f1 . x) + (f2 . x)) by RFUNCT_1:19
.= (f . x) + (f4 . x) by A10, A2, Def44
.= (f <++> f4) . x by A8, A7, Def44 ; :: thesis: verum