theorem :: RVSUM_1:12

for F being real-valued FinSequence holds (<*> REAL) + F = <*> REAL