theorem :: RVSUM_1:10

compreal is_distributive_wrt addreal by Th8, Th9, FINSEQOP:63;