theorem :: RVSUM_1:4

sqrreal is_distributive_wrt multreal