let x1, x2 be set ; :: thesis:
assume that
A1: x1 in dom exp_R and
A2: x2 in dom exp_R and
A3: exp_R . x1 = exp_R . x2 ; :: thesis:
reconsider p1 = x1 as Real by A1;
reconsider p2 = x2 as Real by A2;
thus x1 = log number_e ,(exp_R . p1) by Th13
.= log number_e ,(exp_R . p2) by A3
.= x2 by Th13 ; :: thesis:

end;

hence exp_R is one-to-one by FUNCT_1:def 8; :: thesis:
thus ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL ) by SIN_COS:71; :: thesis:
thus for x being Real holds diff exp_R ,x = exp_R . x by SIN_COS:71; :: thesis:

hereby :: thesis:

let x be Real; :: thesis:
diff exp_R ,x = exp_R . x by SIN_COS:71;
hence diff exp_R ,x > 0 by SIN_COS:59; :: thesis:

end;

thus ( dom exp_R = [#] REAL & dom exp_R = [#] REAL ) by SIN_COS:51; :: thesis:
thus rng exp_R = right_open_halfline 0 :: thesis:

let y be set ; :: thesis:
assume A4: y in rng exp_R ; :: thesis:
consider x being set such that
A5: x in dom exp_R and
A6: y = exp_R . x by A4, FUNCT_1:def 5;
reconsider x = x as Real by A5;
reconsider y1 = y as Real by A6;
exp_R . x > 0 by SIN_COS:59;
then y1 in { g where g is Real : 0 < g } by A6;
hence y in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

then A7: rng exp_R c= right_open_halfline 0 by TARSKI:def 3;

let y be set ; :: thesis:
assume A8: y in right_open_halfline 0 ; :: thesis:
y in { g where g is Real : 0 < g } by A8, XXREAL_1:230;
then consider g being Real such that
A9: ( y = g & 0 < g ) ;
reconsider y1 = y as Real by A9;
y1 = exp_R . (log number_e ,y1) by A9, Th15;
hence y in rng exp_R by FUNCT_1:def 5, SIN_COS:51; :: thesis:

end;

then right_open_halfline 0 c= rng exp_R by TARSKI:def 3;
hence rng exp_R = right_open_halfline 0 by A7, XBOOLE_0:def 10; :: thesis:

end;