let a, b be Real; :: thesis: a * b = (R_EAL a) * (R_EAL b)
( R_EAL a = a & R_EAL b = b ) by MEASURE6:def 1;
hence a * b = (R_EAL a) * (R_EAL b) by Th13; :: thesis: verum