let S be RealNormSpace; :: thesis: for h being PartFunc of REAL, the carrier of S
for seq being Real_Sequence
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
let h be PartFunc of REAL, the carrier of S; :: thesis: for seq being Real_Sequence
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
let seq be Real_Sequence; :: thesis: for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
let r be Real; :: thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r * (h /* seq) )
assume A1: rng seq c= dom h ; :: thesis: (r (#) h) /* seq = r * (h /* seq)
then A2: rng seq c= dom (r (#) h) by VFUNCT_1:def 4;

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

let n be Nat; :: thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n)
A3: n in NAT by ORDINAL1:def 12;
A4: seq . n in dom (r (#) h) by A2, Th1;
thus ((r (#) h) /* seq) . n = (r (#) h) /. (seq . n) by A2, FUNCT_2:109, A3
.= r * (h /. (seq . n)) by A4, VFUNCT_1:def 4
.= r * ((h /* seq) . n) by A1, FUNCT_2:109, A3 ; :: thesis: verum

end;

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