let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: |.(f1 (#) f2).| = |.f1.| (#) |.f2.|
A1: dom |.(f1 (#) f2).| = dom (f1 (#) f2) by VALUED_1:def 11
.= (dom f1) /\ (dom f2) by Th5
.= (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 ;

now

A2: dom |.f2.| = dom f2 by VALUED_1:def 11;
let c be Element of C; :: thesis: ( c in dom |.(f1 (#) f2).| implies |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c )
A3: dom |.f1.| = dom f1 by VALUED_1:def 11;
assume A4: c in dom |.(f1 (#) f2).| ; :: thesis: |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c
then A5: c in dom (f1 (#) f2) by VALUED_1:def 11;
A6: c in (dom |.f1.|) /\ (dom |.f2.|) by A1, A4, VALUED_1:def 4;
then c in dom |.f1.| by XBOOLE_0:def 4;
then A7: f1 . c = f1 /. c by A3, PARTFUN1:def 8;
c in dom |.f2.| by A6, XBOOLE_0:def 4;
then A8: f2 /. c = f2 . c by A2, PARTFUN1:def 8;
thus |.(f1 (#) f2).| . c = |.((f1 (#) f2) . c).| by VALUED_1:18
.= |.((f1 (#) f2) /. c).| by A5, PARTFUN1:def 8
.= |.((f1 /. c) * (f2 /. c)).| by A5, Th5
.= |.(f1 /. c).| * |.(f2 /. c).| by COMPLEX1:151
.= (|.f1.| . c) * |.(f2 /. c).| by A7, VALUED_1:18
.= (|.f1.| . c) * (|.f2.| . c) by A8, VALUED_1:18
.= (|.f1.| (#) |.f2.|) . c by VALUED_1:5 ; :: thesis: verum

end;

hence |.(f1 (#) f2).| = |.f1.| (#) |.f2.| by A1, PARTFUN1:34; :: thesis: verum