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

now

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

end;

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