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: dom h = NAT by FUNCT_2:def 1;
then A2: dom (r (#) h) = NAT by VFUNCT_1:def 4;

now :: thesis: for n being Nat holds (r (#) h) . n = r * (h . n)

let n be Nat; :: thesis: (r (#) h) . n = r * (h . n)
A3: n in NAT by ORDINAL1:def 12;
then (r (#) h) . n = (r (#) h) /. n by A2, PARTFUN1:def 6;
then (r (#) h) . n = r * (h /. n) by A2, VFUNCT_1:def 4, A3;
hence (r (#) h) . n = r * (h . n) by A3, PARTFUN1:def 6, A1; :: thesis: verum

end;

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