let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V
for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let f be PartFunc of C,V; :: thesis: for r being Real holds ||.(r (#) f).|| = (abs r) (#) ||.f.||
let r be Real; :: thesis: ||.(r (#) f).|| = (abs 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 ((abs r) (#) ||.f.||) by VALUED_1:def 5 ;

now

let c be Element of C; :: thesis: ( c in dom ||.(r (#) f).|| implies ||.(r (#) f).|| . c = ((abs r) (#) ||.f.||) . c )
assume A2: c in dom ||.(r (#) f).|| ; :: thesis: ||.(r (#) f).|| . c = ((abs 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
.= (abs r) * ||.(f /. c).|| by NORMSP_1:def 1
.= (abs r) * (||.f.|| . c) by A3, NORMSP_0:def 3
.= ((abs r) (#) ||.f.||) . c by A1, A2, VALUED_1:def 5 ; :: thesis: verum

end;

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