now :: thesis:

let x1, x2 be object ; :: 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 p2 = x2 as Real by A2;
reconsider p1 = x1 as Real by A1;
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 4; :: thesis:
thus ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL ) by SIN_COS:66; :: thesis:
thus for x being Real holds diff (exp_R,x) = exp_R . x by SIN_COS:66; :: thesis:

hereby :: thesis:

let x be Real; :: thesis:
diff (exp_R,x) = exp_R . x by SIN_COS:66;
hence diff (exp_R,x) > 0 by SIN_COS:54; :: thesis:

end;

thus dom exp_R = [#] REAL by SIN_COS:47; :: thesis:

now :: thesis:

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

end;

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

now :: thesis:

let y be object ; :: thesis:
assume y in right_open_halfline 0 ; :: thesis:
then y in { g where g is Real : 0 < g } by XXREAL_1:230;
then A7: ex g being Real st
( y = g & 0 < g ) ;
then reconsider y1 = y as Real ;
A8: log (number_e,y1) in REAL by XREAL_0:def 1;
y1 = exp_R . (log (number_e,y1)) by A7, Th15;
hence y in rng exp_R by FUNCT_1:def 3, SIN_COS:47, A8; :: thesis:

end;

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