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 Th32; :: thesis: verum