A3: ( dom exp_R = REAL & exp_R | REAL is continuous ) by Th71, FDIFF_1:33, FUNCT_2:def 1;
thus exp_R is continuous by A3, RELAT_1:98; :: thesis: verum