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