theorem Th3: :: RVSUM_1:3

multreal is_distributive_wrt addreal