theorem :: RVSUM_1:11
for s being set
for i being natural Number
for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s)