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

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 )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;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

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 )

thus
dom exp_R = [#] REAL
by SIN_COS:47; :: thesis: rng exp_R = right_open_halfline 0let 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;diff (exp_R,x) = exp_R . x by SIN_COS:66;

hence diff (exp_R,x) > 0 by SIN_COS:54; :: thesis: verum

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

y in right_open_halfline 0

then A6:
rng exp_R c= right_open_halfline 0
by TARSKI:def 3;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;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

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

y in rng exp_R

then
right_open_halfline 0 c= rng exp_R
by TARSKI:def 3;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;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

hence rng exp_R = right_open_halfline 0 by A6, XBOOLE_0:def 10; :: thesis: verum