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 ;
thus ((r (#) h) /* seq) . n = (r (#) h) /. (seq . n) by
.= r * (h /. (seq . n)) by
.= r * ((h /* seq) . n) by ; :: thesis: verum
end;
hence (r (#) h) /* seq = r * (h /* seq) by NORMSP_1:def 5; :: thesis: verum