let f, g be complex-valued Function; :: thesis: (f (#) g) " = (f ") (#) (g ")
A1: dom ((f (#) g) ") = dom (f (#) g) by VALUED_1:def 7;
A2: dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def 4;
( dom (f ") = dom f & dom (g ") = dom g ) by VALUED_1:def 7;
hence A3: dom ((f (#) g) ") = dom ((f ") (#) (g ")) by A1, A2, VALUED_1:def 4; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 ((f (#) g) ") or ((f (#) g) ") . b₁ = ((f ") (#) (g ")) . b₁ )
let x be object ; :: thesis: ( not x in proj1 ((f (#) g) ") or ((f (#) g) ") . x = ((f ") (#) (g ")) . x )
assume A4: x in dom ((f (#) g) ") ; :: thesis: ((f (#) g) ") . x = ((f ") (#) (g ")) . x
then A5: (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def 4;
A6: ( (f ") . x = (f . x) " & (g ") . x = (g . x) " ) by VALUED_1:10;
thus ((f (#) g) ") . x = ((f (#) g) . x) " by A4, VALUED_1:def 7
.= ((f . x) ") * ((g . x) ") by A5, XCMPLX_1:204
.= ((f ") (#) (g ")) . x by A3, A4, A6, VALUED_1:def 4 ; :: thesis: verum