let r, r1 be Real; :: thesis: [r1,(r1 * r)] in multRel (REAL,r)
( r1 in REAL & r1 * r in REAL ) by XREAL_0:def 1;
hence [r1,(r1 * r)] in multRel (REAL,r) by Th42; :: thesis: verum