let C be non empty set ; :: thesis: for V being non empty RealNormSpace-like NORMSTR
for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let V be non empty RealNormSpace-like NORMSTR ; :: thesis: for f1 being PartFunc of C,REAL
for f2 being PartFunc of C,V holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let f1 be PartFunc of C,REAL; :: thesis: for f2 being PartFunc of C,V holds ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
let f2 be PartFunc of C,V; :: thesis: ||.(f1 (#) f2).|| = (abs f1) (#) ||.f2.||
A1: dom ||.(f1 (#) f2).|| = dom (f1 (#) f2) by NORMSP_0:def 3
.= (dom f1) /\ (dom f2) by Def3
.= (dom f1) /\ (dom ||.f2.||) by NORMSP_0:def 3
.= (dom (abs f1)) /\ (dom ||.f2.||) by VALUED_1:def 11
.= dom ((abs f1) (#) ||.f2.||) by VALUED_1:def 4 ;

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

let c be Element of C; :: thesis: ( c in dom ||.(f1 (#) f2).|| implies ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c )
assume A2: c in dom ||.(f1 (#) f2).|| ; :: thesis: ||.(f1 (#) f2).|| . c = ((abs f1) (#) ||.f2.||) . c
then A3: c in dom (f1 (#) f2) by NORMSP_0:def 3;
c in (dom (abs f1)) /\ (dom ||.f2.||) by A1, A2, VALUED_1:def 4;
then A4: c in dom ||.f2.|| by XBOOLE_0:def 4;
thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A2, NORMSP_0:def 3
.= ||.((f1 . c) * (f2 /. c)).|| by A3, Def3
.= |.(f1 . c).| * ||.(f2 /. c).|| by NORMSP_1:def 1
.= ((abs f1) . c) * ||.(f2 /. c).|| by VALUED_1:18
.= ((abs f1) . c) * (||.f2.|| . c) by A4, NORMSP_0:def 3
.= ((abs f1) (#) ||.f2.||) . c by VALUED_1:5 ; :: thesis: verum

end;

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