theorem Th71: :: RVSUM_1:71

for F being FinSequence of REAL holds Sum F = addreal $$ F