theorem Th93: :: RVSUM_1:93

for F being FinSequence of REAL holds Product F = multreal $$ F