theorem :: RVSUM_1:28

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