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 <##> 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 <##> 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 <##> f2)
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds (f <//> f1) <//> f2 = f <//> (f1 <##> f2)
let f2 be PartFunc of X2,Y2; :: thesis: (f <//> f1) <//> f2 = f <//> (f1 <##> f2)
set f3 = f <//> f1;
set f4 = f1 <##> f2;
A3:
dom (f <//> f1) = (dom f) /\ (dom f1)
by Def47;
A4:
dom (f1 <##> f2) = (dom f1) /\ (dom f2)
by Def46;
A5:
dom ((f <//> f1) <//> f2) = (dom (f <//> f1)) /\ (dom f2)
by Def47;
A6:
dom (f <//> (f1 <##> f2)) = (dom f) /\ (dom (f1 <##> f2))
by Def47;
hence A7:
dom ((f <//> f1) <//> f2) = dom (f <//> (f1 <##> f2))
by A3, A5, A4, XBOOLE_1:16; :: according to FUNCT_1:def 17 :: thesis: for b1 being set holds
( not b1 in dom ((f <//> f1) <//> f2) or ((f <//> f1) <//> f2) . b1 = (f <//> (f1 <##> f2)) . b1 )
let x be set ; :: thesis: ( not x in dom ((f <//> f1) <//> f2) or ((f <//> f1) <//> f2) . x = (f <//> (f1 <##> f2)) . x )
assume A8:
x in dom ((f <//> f1) <//> f2)
; :: thesis: ((f <//> f1) <//> f2) . x = (f <//> (f1 <##> f2)) . x
then A9:
x in dom (f <//> f1)
by A5, XBOOLE_0:def 4;
A10:
x in dom (f1 <##> f2)
by A6, A8, A7, XBOOLE_0:def 4;
thus ((f <//> f1) <//> f2) . x =
((f <//> f1) . x) /" (f2 . x)
by A8, Def47
.=
((f . x) /" (f1 . x)) /" (f2 . x)
by A9, Def47
.=
(f . x) /" ((f1 . x) (#) (f2 . x))
by Th14
.=
(f . x) /" ((f1 <##> f2) . x)
by A10, Def46
.=
(f <//> (f1 <##> f2)) . x
by A8, A7, Def47
; :: thesis: verum