theorem :: RVSUM_2:4

for F being complex-valued FinSequence holds (<*> COMPLEX) + F = <*> COMPLEX