theorem :: RVSUM_2:12

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