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 <##> f2) <//> f1

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 <##> f2) <//> f1

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 <##> f2) <//> f1

let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2 holds (f <//> f1) <##> f2 = (f <##> f2) <//> f1
let f2 be PartFunc of X2,Y2; :: thesis: (f <//> f1) <##> f2 = (f <##> f2) <//> f1
set f3 = f <//> f1;
set f4 = f <##> f2;
A1: dom ((f <//> f1) <##> f2) = (dom (f <//> f1)) /\ (dom f2) by Def47;
A2: dom ((f <##> f2) <//> f1) = (dom (f <##> f2)) /\ (dom f1) by Def48;
( dom (f <//> f1) = (dom f) /\ (dom f1) & dom (f <##> f2) = (dom f) /\ (dom f2) ) by ;
hence A3: dom ((f <//> f1) <##> f2) = dom ((f <##> f2) <//> f1) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom ((f <//> f1) <##> f2) or ((f <//> f1) <##> f2) . b1 = ((f <##> f2) <//> f1) . b1 )

let x be object ; :: thesis: ( not x in dom ((f <//> f1) <##> f2) or ((f <//> f1) <##> f2) . x = ((f <##> f2) <//> f1) . x )
assume A4: x in dom ((f <//> f1) <##> f2) ; :: thesis: ((f <//> f1) <##> f2) . x = ((f <##> f2) <//> f1) . x
then A5: x in dom (f <##> f2) by ;
A6: x in dom (f <//> f1) by ;
thus ((f <//> f1) <##> f2) . x = ((f <//> f1) . x) (#) (f2 . x) by
.= ((f . x) /" (f1 . x)) (#) (f2 . x) by
.= ((f . x) (#) (f2 . x)) /" (f1 . x) by Th20
.= ((f <##> f2) . x) /" (f1 . x) by
.= ((f <##> f2) <//> f1) . x by ; :: thesis: verum