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 3
.= ((rseq . n) * (seq1 . n)) - ((rseq . n) * (seq2 . n)) by RLVECT_1:34
.= ((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 3 ; :: thesis: verum
end;
hence rseq (#) (seq1 - seq2) = (rseq (#) seq1) - (rseq (#) seq2) by FUNCT_2:63; :: thesis: verum