let C be non empty set ; :: thesis: for r being Real
for V being non empty RealNormSpace-like NORMSTR
for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||
let r be Real; :: thesis: for V being non empty RealNormSpace-like NORMSTR
for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||
let V be non empty RealNormSpace-like NORMSTR ; :: thesis: for f being PartFunc of C,V holds ||.(r (#) f).|| = |.r.| (#) ||.f.||
let f be PartFunc of C,V; :: thesis: ||.(r (#) f).|| = |.r.| (#) ||.f.||
A1: dom ||.(r (#) f).|| = dom (r (#) f) by NORMSP_0:def 3
.= dom f by Def4
.= dom ||.f.|| by NORMSP_0:def 3
.= dom (|.r.| (#) ||.f.||) by VALUED_1:def 5 ;

now :: thesis: for c being Element of C st c in dom ||.(r (#) f).|| holds
||.(r (#) f).|| . c = (|.r.| (#) ||.f.||) . c

let c be Element of C; :: thesis: ( c in dom ||.(r (#) f).|| implies ||.(r (#) f).|| . c = (|.r.| (#) ||.f.||) . c )
assume A2: c in dom ||.(r (#) f).|| ; :: thesis: ||.(r (#) f).|| . c = (|.r.| (#) ||.f.||) . c
then A3: c in dom ||.f.|| by A1, VALUED_1:def 5;
A4: c in dom (r (#) f) by A2, NORMSP_0:def 3;
thus ||.(r (#) f).|| . c = ||.((r (#) f) /. c).|| by A2, NORMSP_0:def 3
.= ||.(r * (f /. c)).|| by A4, Def4
.= |.r.| * ||.(f /. c).|| by NORMSP_1:def 1
.= |.r.| * (||.f.|| . c) by A3, NORMSP_0:def 3
.= (|.r.| (#) ||.f.||) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

hence ||.(r (#) f).|| = |.r.| (#) ||.f.|| by A1, PARTFUN1:5; :: thesis: verum