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

now

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 c in (dom (abs f1)) /\ (dom ||.f2.||) by A1, VALUED_1:def 4;
then A3: ( c in dom (abs f1) & c in dom ||.f2.|| ) by XBOOLE_0:def 4;
A4: c in dom (f1 (#) f2) by A2, Def5;
thus ||.(f1 (#) f2).|| . c = ||.((f1 (#) f2) /. c).|| by A2, Def5
.= ||.((f1 . c) * (f2 /. c)).|| by A4, Def3
.= (abs (f1 . c)) * ||.(f2 /. c).|| by NORMSP_1:def 2
.= ((abs f1) . c) * ||.(f2 /. c).|| by VALUED_1:18
.= ((abs f1) . c) * (||.f2.|| . c) by A3, Def5
.= ((abs f1) (#) ||.f2.||) . c by VALUED_1:5 ; :: thesis: verum

end;

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