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) + (- (rseq2 . n))) * (seq . n) by SEQ_1:10
.= ((rseq1 . n) - (rseq2 . n)) * (seq . n)
.= ((rseq1 . n) * (seq . n)) - ((rseq2 . n) * (seq . n)) by RLVECT_1:35
.= ((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 3 ; :: thesis: verum

end;

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