let r be Real; :: thesis: r multreal is_distributive_wrt addreal
r in REAL by XREAL_0:def 1;
hence r multreal is_distributive_wrt addreal by Th3, FINSEQOP:54; :: thesis: verum