let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let V be ComplexNormSpace; :: thesis: for f2 being PartFunc of M,V
for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let f2 be PartFunc of M,V; :: thesis: for f1 being PartFunc of M,COMPLEX holds ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
let f1 be PartFunc of M,COMPLEX; :: thesis: ||.(f1 (#) f2).|| = |.f1.| (#) ||.f2.||
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def1;
A2: (dom f1) /\ (dom f2) = (dom f1) /\ (dom ||.f2.||) by NORMSP_0:def 3
.= (dom |.f1.|) /\ (dom ||.f2.||) by VALUED_1:def 11
.= dom (|.f1.| (#) ||.f2.||) by VALUED_1:def 4 ;
A3: dom ||.(f1 (#) f2).|| = dom (f1 (#) f2) by NORMSP_0:def 3;

now :: thesis: for c being Element of M st c in dom ||.(f1 (#) f2).|| holds
||.(f1 (#) f2).|| . c = (|.f1.| (#) ||.f2.||) . c

let c be Element of M; :: thesis: ( c in dom ||.(f1 (#) f2).|| implies ||.(f1 (#) f2).|| . c = (|.f1.| (#) ||.f2.||) . c )
assume A4: c in dom ||.(f1 (#) f2).|| ; :: thesis: ||.(f1 (#) f2).|| . c = (|.f1.| (#) ||.f2.||) . c
then c in (dom |.f1.|) /\ (dom ||.f2.||) by A3, A1, A2, VALUED_1:def 4;
then A5: c in dom ||.f2.|| by XBOOLE_0:def 4;
A6: c in dom (f1 (#) f2) by A4, NORMSP_0:def 3;
then c in dom f1 by A1, XBOOLE_0:def 4;
then A7: f1 /. c = f1 . c by PARTFUN1:def 6;
thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A4, NORMSP_0:def 3
.= ||.((f1 /. c) * (f2 /. c)).|| by A6, Def1
.= |.(f1 /. c).| * ||.(f2 /. c).|| by CLVECT_1:def 13
.= (|.f1.| . c) * ||.(f2 /. c).|| by A7, VALUED_1:18
.= (|.f1.| . c) * (||.f2.|| . c) by A5, NORMSP_0:def 3
.= (|.f1.| (#) ||.f2.||) . c by VALUED_1:5 ; :: thesis: verum

end;

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