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)

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

hence
r * (rseq (#) seq) = rseq (#) (r * seq)
by FUNCT_2:63; :: thesis: verumlet 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;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