A1: {0,+infty} misses ].0,+infty.[ by XXREAL_1:86;
0 in {0,+infty} by TARSKI:def 2;
then not 0 in ].0,+infty.[ by A1, XBOOLE_0:def 4;
then A3: not 0 in rng exp_R by TAYLOR_1:16, LIMFUNC1:def 3;
then A4: exp_R " {0} = {} by FUNCT_1:72;
dom (exp_R ^) = (dom exp_R) \ (exp_R " {0}) by RFUNCT_1:def 2
.= REAL by A4, FUNCT_2:def 1 ;
hence ( dom (exp_R ^) = REAL & exp_R " {0} = {} ) by A3, FUNCT_1:72; :: thesis: verum