theorem :: RVSUM_1:27

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)