let a, b be Real; :: thesis: a * b = (R_EAL a) * (R_EAL b)
reconsider a = a, b = b as real number ;
( 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