let f1, f2 be complex-valued Function; :: thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by Def2
.= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by Th2
.= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0})) by Def2
.= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2
.= dom ((f1 ^) (#) (f2 ^)) by VALUED_1:def 4 ;

now :: thesis: for c being object st c in dom ((f1 (#) f2) ^) holds
((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c

let c be object ; :: thesis: ( c in dom ((f1 (#) f2) ^) implies ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c )
assume A2: c in dom ((f1 (#) f2) ^) ; :: thesis: ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c
then A3: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, VALUED_1:def 4;
then A4: c in dom (f1 ^) by XBOOLE_0:def 4;
A5: c in dom (f2 ^) by A3, XBOOLE_0:def 4;
thus ((f1 (#) f2) ^) . c = ((f1 (#) f2) . c) " by A2, Def2
.= ((f1 . c) * (f2 . c)) " by VALUED_1:5
.= ((f1 . c) ") * ((f2 . c) ") by XCMPLX_1:204
.= ((f1 ^) . c) * ((f2 . c) ") by A4, Def2
.= ((f1 ^) . c) * ((f2 ^) . c) by A5, Def2
.= ((f1 ^) (#) (f2 ^)) . c by VALUED_1:5 ; :: thesis: verum

end;

hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, FUNCT_1:2; :: thesis: verum