now :: thesis: for x1, x2 being object st x1 in dom exp_R & x2 in dom exp_R & exp_R . x1 = exp_R . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom exp_R & x2 in dom exp_R & exp_R . x1 = exp_R . x2 implies x1 = x2 )
assume that
A1: x1 in dom exp_R and
A2: x2 in dom exp_R and
A3: exp_R . x1 = exp_R . x2 ; :: thesis: x1 = x2
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: verum

end;

hence exp_R is one-to-one by FUNCT_1:def 4; :: thesis: ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
thus ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL ) by SIN_COS:66; :: thesis: ( ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
thus for x being Real holds diff (exp_R,x) = exp_R . x by SIN_COS:66; :: thesis: ( ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )

hereby :: thesis: ( dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )

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

end;

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

now :: thesis: for y being object st y in rng exp_R holds
y in right_open_halfline 0

let y be object ; :: thesis: ( y in rng exp_R implies y in right_open_halfline 0 )
assume y in rng exp_R ; :: thesis: y in right_open_halfline 0
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: verum

end;

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

now :: thesis: for y being object st y in right_open_halfline 0 holds
y in rng exp_R

let y be object ; :: thesis: ( y in right_open_halfline 0 implies y in rng exp_R )
assume y in right_open_halfline 0 ; :: thesis: y in rng exp_R
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: verum

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: verum