let f1, f2 be complex-valued Function; :: thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " ) by Def2
.= ((dom f1) \ (f1 " )) /\ ((dom f2) \ (f2 " )) by Th2
.= (dom (f1 ^)) /\ ((dom f2) \ (f2 " )) 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 ;
then A4: c in dom (f1 ^) by XBOOLE_0:def 4;
A5: c in dom (f2 ^) by ;
thus ((f1 (#) f2) ^) . c = ((f1 (#) f2) . c) " by
.= ((f1 . c) * (f2 . c)) " by VALUED_1:5
.= ((f1 . c) ") * ((f2 . c) ") by XCMPLX_1:204
.= ((f1 ^) . c) * ((f2 . c) ") by
.= ((f1 ^) . c) * ((f2 ^) . c) by
.= ((f1 ^) (#) (f2 ^)) . c by VALUED_1:5 ; :: thesis: verum
end;
hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by ; :: thesis: verum