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

now

let c be set ; :: 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, Def8
.= ((f1 . c) * (f2 . c)) " by VALUED_1:5
.= ((f1 . c) " ) * ((f2 . c) " ) by XCMPLX_1:205
.= ((f1 ^ ) . c) * ((f2 . c) " ) by A4, Def8
.= ((f1 ^ ) . c) * ((f2 ^ ) . c) by A5, Def8
.= ((f1 ^ ) (#) (f2 ^ )) . c by VALUED_1:5 ; :: thesis: verum

end;

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