let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X holds Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)
let seq1, seq2 be sequence of X; :: thesis: Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2)

now

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 Def9
.= (Rseq . n) * ((seq1 . n) + (seq2 . n)) by NORMSP_1:def 5
.= ((Rseq . n) * (seq1 . n)) + ((Rseq . n) * (seq2 . n)) by RLVECT_1:def 9
.= ((Rseq * seq1) . n) + ((Rseq . n) * (seq2 . n)) by Def9
.= ((Rseq * seq1) . n) + ((Rseq * seq2) . n) by Def9
.= ((Rseq * seq1) + (Rseq * seq2)) . n by NORMSP_1:def 5 ; :: thesis: verum

end;

hence Rseq * (seq1 + seq2) = (Rseq * seq1) + (Rseq * seq2) by FUNCT_2:113; :: thesis: verum