let f1, f2 be complex-valued Function; :: thesis: |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
thus dom |.(f1 (#) f2).| = dom (f1 (#) f2) by VALUED_1:def 11
.= (dom f1) /\ (dom f2) by VALUED_1:def 4
.= (dom f1) /\ (dom |.f2.|) by VALUED_1:def 11
.= (dom |.f1.|) /\ (dom |.f2.|) by VALUED_1:def 11
.= dom (|.f1.| (#) |.f2.|) by VALUED_1:def 4 ; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom |.(f1 (#) f2).| or |.(f1 (#) f2).| . b₁ = (|.f1.| (#) |.f2.|) . b₁ )
let c be object ; :: thesis: ( not c in dom |.(f1 (#) f2).| or |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c )
assume c in dom |.(f1 (#) f2).| ; :: thesis: |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c
then A5: c in dom (f1 (#) f2) by VALUED_1:def 11;
thus |.(f1 (#) f2).| . c = |.((f1 (#) f2) . c).| by VALUED_1:18
.= |.((f1 . c) * (f2 . c)).| by A5, VALUED_1:def 4
.= |.(f1 . c).| * |.(f2 . c).| by COMPLEX1:65
.= (|.f1.| . c) * |.(f2 . c).| by VALUED_1:18
.= (|.f1.| . c) * (|.f2.| . c) by VALUED_1:18
.= (|.f1.| (#) |.f2.|) . c by VALUED_1:5 ; :: thesis: verum