theorem :: RVSUM_1:52

for F being real-valued FinSequence holds 1 * F = F by RFUNCT_1:21;