let Rseq1, Rseq2 be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let X be RealUnitarySpace; :: thesis: for seq being sequence of X holds (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let seq be sequence of X; :: thesis: (Rseq1 + Rseq2) * seq = (Rseq1 * seq) + (Rseq2 * seq)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: K64(((Rseq1 + Rseq2) * seq),n) = K64(((Rseq1 * seq) + (Rseq2 * seq)),n)
thus ((Rseq1 + Rseq2) * seq) . n = ((Rseq1 + Rseq2) . n) * (seq . n) by Def7
.= ((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 Def7
.= ((Rseq1 * seq) . n) + ((Rseq2 * seq) . n) by Def7
.= ((Rseq1 * seq) + (Rseq2 * seq)) . n by NORMSP_1:def 2 ; :: thesis: verum