let X, X1, X2 be set ; :: thesis: for Y, Y1, Y2 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 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)
let Y, Y1, Y2 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 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)
let f2 be PartFunc of X2,Y2; :: thesis: f <##> (f1 <--> f2) = (f <##> f1) <--> (f <##> f2)
set f3 = f <##> f1;
set f4 = f <##> f2;
set f5 = f1 <--> f2;
A1: dom (f <##> (f1 <--> f2)) = (dom f) /\ (dom (f1 <--> f2)) by Def47;
A2: dom (f1 <--> f2) = (dom f1) /\ (dom f2) by Def46;
A3: dom ((f <##> f1) <--> (f <##> f2)) = (dom (f <##> f1)) /\ (dom (f <##> f2)) by Def46;
( dom (f <##> f1) = (dom f) /\ (dom f1) & dom (f <##> f2) = (dom f) /\ (dom f2) ) by Def47;
hence A4: dom (f <##> (f1 <--> f2)) = dom ((f <##> f1) <--> (f <##> f2)) by A1, A3, A2, Lm1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (f <##> (f1 <--> f2)) or (f <##> (f1 <--> f2)) . b₁ = ((f <##> f1) <--> (f <##> f2)) . b₁ )
let x be object ; :: thesis: ( not x in dom (f <##> (f1 <--> f2)) or (f <##> (f1 <--> f2)) . x = ((f <##> f1) <--> (f <##> f2)) . x )
assume A5: x in dom (f <##> (f1 <--> f2)) ; :: thesis: (f <##> (f1 <--> f2)) . x = ((f <##> f1) <--> (f <##> f2)) . x
then A6: x in dom (f <##> f1) by A3, A4, XBOOLE_0:def 4;
A7: x in dom (f1 <--> f2) by A1, A5, XBOOLE_0:def 4;
A8: x in dom (f <##> f2) by A3, A4, A5, XBOOLE_0:def 4;
thus (f <##> (f1 <--> f2)) . x = (f . x) (#) ((f1 <--> f2) . x) by A5, Def47
.= (f . x) (#) ((f1 . x) - (f2 . x)) by A7, Def46
.= ((f . x) (#) (f1 . x)) - ((f . x) (#) (f2 . x)) by RFUNCT_1:15
.= ((f <##> f1) . x) - ((f . x) (#) (f2 . x)) by A6, Def47
.= ((f <##> f1) . x) - ((f <##> f2) . x) by A8, Def47
.= ((f <##> f1) <--> (f <##> f2)) . x by A4, A5, Def46 ; :: thesis: verum