let f1, f2, f3 be complex-valued Function; :: thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3)
A1: dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by VALUED_1:def 4
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def 4 ;
A2: dom (f1 (#) (f2 (#) f3)) = (dom f1) /\ (dom (f2 (#) f3)) by VALUED_1:def 4
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def 4 ;
then A3: dom ((f1 (#) f2) (#) f3) = dom (f1 (#) (f2 (#) f3)) by A1, XBOOLE_1:16;
for x being object st x in dom ((f1 (#) f2) (#) f3) holds
((f1 (#) f2) (#) f3) . x = (f1 (#) (f2 (#) f3)) . x

proof

let x be object ; :: thesis: ( x in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) . x = (f1 (#) (f2 (#) f3)) . x )
assume B1: x in dom ((f1 (#) f2) (#) f3) ; :: thesis: ((f1 (#) f2) (#) f3) . x = (f1 (#) (f2 (#) f3)) . x
x in dom (f1 (#) (f2 (#) f3)) by B1, A1, A2, XBOOLE_1:16;
then B2a: ( x in (dom (f1 (#) f2)) /\ (dom f3) & x in (dom f1) /\ (dom (f2 (#) f3)) ) by VALUED_1:def 4, B1;
B3: ((f1 (#) f2) (#) f3) . x = ((f1 (#) f2) . x) * (f3 . x) by VALUED_1:def 4, B1
.= ((f1 . x) * (f2 . x)) * (f3 . x) by B2a, VALUED_1:def 4 ;
(f1 (#) (f2 (#) f3)) . x = (f1 . x) * ((f2 (#) f3) . x) by A3, B1, VALUED_1:def 4
.= (f1 . x) * ((f2 . x) * (f3 . x)) by B2a, VALUED_1:def 4 ;
hence ((f1 (#) f2) (#) f3) . x = (f1 (#) (f2 (#) f3)) . x by B3; :: thesis: verum

end;

hence (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, A2, XBOOLE_1:16, FUNCT_1:2; :: thesis: verum