let S be RealNormSpace; :: thesis: for rseq being Real_Sequence
for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
let rseq be Real_Sequence; :: thesis: for seq1, seq2 being sequence of S holds rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)
let seq1, seq2 be sequence of S; :: thesis: rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2)

now :: thesis: for n being Element of NAT holds (rseq (#) (seq1 + seq2)) . n = ((rseq (#) seq1) + (rseq (#) seq2)) . n

let n be Element of NAT ; :: thesis: (rseq (#) (seq1 + seq2)) . n = ((rseq (#) seq1) + (rseq (#) seq2)) . n
thus (rseq (#) (seq1 + seq2)) . n = (rseq . n) * ((seq1 + seq2) . n) by Def2
.= (rseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def 2
.= ((rseq . n) * (seq1 . n)) + ((rseq . n) * (seq2 . n)) by RLVECT_1:def 5
.= ((rseq (#) seq1) . n) + ((rseq . n) * (seq2 . n)) by Def2
.= ((rseq (#) seq1) . n) + ((rseq (#) seq2) . n) by Def2
.= ((rseq (#) seq1) + (rseq (#) seq2)) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence rseq (#) (seq1 + seq2) = (rseq (#) seq1) + (rseq (#) seq2) by FUNCT_2:63; :: thesis: verum