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
Y0: rng (r (#) h) c= the carrier of S ;
dom h = NAT by FUNCT_2:def 1;
then X3: dom (r (#) h) = NAT by VFUNCT_1:def 4;
then X0: r (#) h is sequence of S by Y0, FUNCT_2:4;

now

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

end;

hence r (#) h = r * h by X0, NORMSP_1:def 8; :: thesis: verum