let S be RealNormSpace; :: thesis: for h being sequence of S
for r being Real holds r (#) h = r * h
let h be sequence of S; :: thesis: for r being Real holds r (#) h = r * h
let r be Real; :: thesis: r (#) h = r * h
dom h = NAT by FUNCT_2:def 1;
then A1: dom (r (#) h) = NAT by VFUNCT_1:def 4;

now :: thesis: for n being Element of NAT holds (r (#) h) . n = r * (h . n)

let n be Element of NAT ; :: thesis: (r (#) h) . n = r * (h . n)
(r (#) h) . n = (r (#) h) /. n ;
then (r (#) h) . n = r * (h /. n) by A1, VFUNCT_1:def 4;
hence (r (#) h) . n = r * (h . n) ; :: thesis: verum

end;

hence r (#) h = r * h by NORMSP_1:def 5; :: thesis: verum