for r being Real holds r multreal is_distributive_wrt addreal