let r be Real; :: thesis: for S being RealNormSpace
for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let S be RealNormSpace; :: thesis: for seq being sequence of S
for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let seq be sequence of S; :: thesis: for rseq being Real_Sequence holds r * (rseq (#) seq) = rseq (#) (r * seq)
let rseq be Real_Sequence; :: thesis: r * (rseq (#) seq) = rseq (#) (r * seq)

now :: thesis: for n being Element of NAT holds (r * (rseq (#) seq)) . n = (rseq (#) (r * seq)) . n

let n be Element of NAT ; :: thesis: (r * (rseq (#) seq)) . n = (rseq (#) (r * seq)) . n
thus (r * (rseq (#) seq)) . n = r * ((rseq (#) seq) . n) by NORMSP_1:def 5
.= r * ((rseq . n) * (seq . n)) by Def2
.= (r * (rseq . n)) * (seq . n) by RLVECT_1:def 7
.= (rseq . n) * (r * (seq . n)) by RLVECT_1:def 7
.= (rseq . n) * ((r * seq) . n) by NORMSP_1:def 5
.= (rseq (#) (r * seq)) . n by Def2 ; :: thesis: verum

end;

hence r * (rseq (#) seq) = rseq (#) (r * seq) by FUNCT_2:63; :: thesis: verum