let S be RealNormSpace; :: thesis: for seq being sequence of S
for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
let seq be sequence of S; :: thesis: for rseq1, rseq2 being Real_Sequence holds (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)
let rseq1, rseq2 be Real_Sequence; :: thesis: (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq)

now :: thesis: for n being Element of NAT holds ((rseq1 + rseq2) (#) seq) . n = ((rseq1 (#) seq) + (rseq2 (#) seq)) . n

let n be Element of NAT ; :: thesis: ((rseq1 + rseq2) (#) seq) . n = ((rseq1 (#) seq) + (rseq2 (#) seq)) . n
thus ((rseq1 + rseq2) (#) seq) . n = ((rseq1 + rseq2) . n) * (seq . n) by Def2
.= ((rseq1 . n) + (rseq2 . n)) * (seq . n) by SEQ_1:7
.= ((rseq1 . n) * (seq . n)) + ((rseq2 . n) * (seq . n)) by RLVECT_1:def 6
.= ((rseq1 (#) seq) . n) + ((rseq2 . n) * (seq . n)) by Def2
.= ((rseq1 (#) seq) . n) + ((rseq2 (#) seq) . n) by Def2
.= ((rseq1 (#) seq) + (rseq2 (#) seq)) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence (rseq1 + rseq2) (#) seq = (rseq1 (#) seq) + (rseq2 (#) seq) by FUNCT_2:63; :: thesis: verum