consider g being PartFunc of REAL,REAL such that
A2: dom g = right_open_halfline 0 and
A3: for x being Real st x in right_open_halfline 0 holds
g . x = log (2,x) and
A4: g is_differentiable_on right_open_halfline 0 and
A5: for x being Real st x in right_open_halfline 0 holds
( g is_differentiable_in x & diff (g,x) = (log (2,number_e)) / x & 0 < diff (g,x) ) by Lm6;
set g0 = g | ;
AA6: for x being object st x in right_open_halfline number_e holds
x in right_open_halfline 0
proof
let x be object ; :: thesis:
assume x in right_open_halfline number_e ; :: thesis:
then x in { y where y is Real : number_e < y } by XXREAL_1:230;
then consider y being Real such that
AA2: ( x = y & number_e < y ) ;
x in { z where z is Real : 0 < z } by ;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
then A6: right_open_halfline number_e c= right_open_halfline 0 ;
then A7: dom () = right_open_halfline number_e by ;
set f = (id ()) / ();
G0: (g | ) " = {}
proof
assume (g | ) " <> {} ; :: thesis: contradiction
then consider x being object such that
P01: x in () " by XBOOLE_0:def 1;
P02: ( x in dom () & () . x in ) by ;
P04: (g | ) . x = 0 by ;
reconsider x0 = x as Real by P01;
x0 in { y where y is Real : number_e < y } by ;
then ex y being Real st
( x = y & number_e < y ) ;
then E5: 2 < x0 by ;
F3: () . x = g . x by
.= log (2,x0) by A3, AA6, P02, A7 ;
log (2,2) <= log (2,x0) by ;
hence contradiction by POWER:52, P04, F3; :: thesis: verum
end;
take (id ()) / () ; :: thesis: ( right_open_halfline number_e = dom ((id ()) / ()) & ( for x being Real st x in dom ((id ()) / ()) holds
((id ()) / ()) . x = x / (log (2,x)) ) & (id ()) / () is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ()) / ()),x0) ) & (id ()) / () is non-decreasing )

thus P1: dom ((id ()) / ()) = (dom (id ())) /\ ((dom ()) \ (() " )) by RFUNCT_1:def 1
.= right_open_halfline number_e by ; :: thesis: ( ( for x being Real st x in dom ((id ()) / ()) holds
((id ()) / ()) . x = x / (log (2,x)) ) & (id ()) / () is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ()) / ()),x0) ) & (id ()) / () is non-decreasing )

thus for x being Real st x in dom ((id ()) / ()) holds
((id ()) / ()) . x = x / (log (2,x)) :: thesis: ( (id ()) / () is_differentiable_on right_open_halfline number_e & ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ()) / ()),x0) ) & (id ()) / () is non-decreasing )
proof
let x be Real; :: thesis: ( x in dom ((id ()) / ()) implies ((id ()) / ()) . x = x / (log (2,x)) )
assume F1: x in dom ((id ()) / ()) ; :: thesis: ((id ()) / ()) . x = x / (log (2,x))
thus ((id ()) / ()) . x = ((id ()) . x) * ((() . x) ") by
.= x * ((() . x) ") by Lm5
.= x * ((g . x) ") by
.= x * ((log (2,x)) ") by A3, P1, AA6, F1
.= x * (1 / (log (2,x))) by XCMPLX_1:215
.= (1 * x) / (log (2,x)) by XCMPLX_1:74
.= x / (log (2,x)) ; :: thesis: verum
end;
P3: g is_differentiable_on right_open_halfline number_e by ;
then XP: ( g | is_differentiable_on right_open_halfline number_e & g `| = () `| ) by FDIFF_2:16;
F12: for x being Real st x in right_open_halfline number_e holds
( (id ()) / () is_differentiable_in x & diff (((id ()) / ()),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) )
proof
let x be Real; :: thesis: ( x in right_open_halfline number_e implies ( (id ()) / () is_differentiable_in x & diff (((id ()) / ()),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) ) )
assume F1: x in right_open_halfline number_e ; :: thesis: ( (id ()) / () is_differentiable_in x & diff (((id ()) / ()),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) )
then FA: x in right_open_halfline 0 by AA6;
FB: diff (g,x) = () . x by
.= diff ((),x) by ;
x in { y where y is Real : number_e < y } by ;
then EE5: ex y being Real st
( x = y & number_e < y ) ;
then E5: 2 < x by ;
F3: () . x = g . x by
.= log (2,x) by F1, AA6, A3 ;
log (2,2) <= log (2,x) by ;
then F2: 0 < () . x by ;
F3: id () is_differentiable_in x by Lm5;
F6: g | is_differentiable_in x by P3, F1;
diff (((id ()) / ()),x) = (((diff ((id ()),x)) * (() . x)) - ((diff ((),x)) * ((id ()) . x))) / ((() . x) ^2) by
.= ((1 * (() . x)) - ((diff ((),x)) * ((id ()) . x))) / ((() . x) ^2) by Lm5
.= ((1 * (() . x)) - ((diff ((),x)) * x)) / ((() . x) ^2) by Lm5
.= ((1 * (g . x)) - ((diff (g,x)) * x)) / ((() . x) ^2) by
.= ((1 * (g . x)) - ((diff (g,x)) * x)) / ((g . x) ^2) by
.= ((1 * (log (2,x))) - ((diff (g,x)) * x)) / ((g . x) ^2) by A3, F1, AA6
.= ((1 * (log (2,x))) - ((diff (g,x)) * x)) / ((log (2,x)) ^2) by A3, AA6, F1
.= ((1 * (log (2,x))) - (((log (2,number_e)) / x) * x)) / ((log (2,x)) ^2) by A5, FA
.= ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) by ;
hence ( (id ()) / () is_differentiable_in x & diff (((id ()) / ()),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) ) by ; :: thesis: verum
end;
hence P3: (id ()) / () is_differentiable_on right_open_halfline number_e by P1; :: thesis: ( ( for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (((id ()) / ()),x0) ) & (id ()) / () is non-decreasing )

thus for x being Real st x in right_open_halfline number_e holds
0 <= diff (((id ()) / ()),x) :: thesis: (id ()) / () is non-decreasing
proof
let x be Real; :: thesis: ( x in right_open_halfline number_e implies 0 <= diff (((id ()) / ()),x) )
assume F1: x in right_open_halfline number_e ; :: thesis: 0 <= diff (((id ()) / ()),x)
then P41: diff (((id ()) / ()),x) = ((log (2,x)) - (log (2,number_e))) / ((log (2,x)) ^2) by F12;
x in { y where y is Real : number_e < y } by ;
then ex y being Real st
( x = y & number_e < y ) ;
then log (2,number_e) < log (2,x) by ;
then 0 < (log (2,x)) - (log (2,number_e)) by XREAL_1:50;
hence 0 <= diff (((id ()) / ()),x) by P41; :: thesis: verum
end;
hence (id ()) / () is non-decreasing by ; :: thesis: verum