theorem :: RVSUM_2:11

for s being set
for i being Nat
for R1, R2 being b₂ -element complex-valued FinSequence holds (R1 - R2) . s = (R1 . s) - (R2 . s)