let X, X1, X2 be set ; 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 <//> f2)
let Y, Y1, Y2 be 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 <//> f2)
let f be PartFunc of X,Y; for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds (f <##> f1) <//> f2 = f <##> (f1 <//> f2)
let f1 be PartFunc of X1,Y1; for f2 being PartFunc of X2,Y2 holds (f <##> f1) <//> f2 = f <##> (f1 <//> f2)
let f2 be PartFunc of X2,Y2; (f <##> f1) <//> f2 = f <##> (f1 <//> f2)
set f3 = f <##> f1;
set f4 = f1 <//> f2;
A1:
dom ((f <##> f1) <//> f2) = (dom (f <##> f1)) /\ (dom f2)
by Def48;
A2:
dom (f <##> (f1 <//> f2)) = (dom f) /\ (dom (f1 <//> f2))
by Def47;
( dom (f <##> f1) = (dom f) /\ (dom f1) & dom (f1 <//> f2) = (dom f1) /\ (dom f2) )
by Def47, Def48;
hence A3:
dom ((f <##> f1) <//> f2) = dom (f <##> (f1 <//> f2))
by A1, A2, XBOOLE_1:16; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom ((f <##> f1) <//> f2) or ((f <##> f1) <//> f2) . b1 = (f <##> (f1 <//> f2)) . b1 )
let x be object ; ( not x in dom ((f <##> f1) <//> f2) or ((f <##> f1) <//> f2) . x = (f <##> (f1 <//> f2)) . x )
assume A4:
x in dom ((f <##> f1) <//> f2)
; ((f <##> f1) <//> f2) . x = (f <##> (f1 <//> f2)) . x
then A5:
x in dom (f1 <//> f2)
by A2, A3, XBOOLE_0:def 4;
A6:
x in dom (f <##> f1)
by A1, A4, XBOOLE_0:def 4;
thus ((f <##> f1) <//> f2) . x =
((f <##> f1) . x) /" (f2 . x)
by A4, Def48
.=
((f . x) (#) (f1 . x)) /" (f2 . x)
by A6, Def47
.=
(f . x) (#) ((f1 . x) /" (f2 . x))
by Th19
.=
(f . x) (#) ((f1 <//> f2) . x)
by A5, Def48
.=
(f <##> (f1 <//> f2)) . x
by A3, A4, Def47
; verum