set g = (log (2,number_e)) (#) ln;
take (log (2,number_e)) (#) ln ; :: thesis: ( dom ((log (2,number_e)) (#) ln) = right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

thus A3: dom ((log (2,number_e)) (#) ln) = dom ln by VALUED_1:def 5
.= right_open_halfline 0 by TAYLOR_1:def 2 ; :: thesis: ( ( for x being Real st x in right_open_halfline 0 holds
((log (2,number_e)) (#) ln) . x = log (2,x) ) & (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )

E1: number_e > 1 by ;
thus for d being Real st d in right_open_halfline 0 holds
((log (2,number_e)) (#) ln) . d = log (2,d) :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x in right_open_halfline 0 holds
( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) ) )
proof
let d be Real; :: thesis: ( d in right_open_halfline 0 implies ((log (2,number_e)) (#) ln) . d = log (2,d) )
assume A51: d in right_open_halfline 0 ; :: thesis: ((log (2,number_e)) (#) ln) . d = log (2,d)
then reconsider d0 = d as Element of right_open_halfline 0 ;
d in { y where y is Real : 0 < y } by ;
then E3: ex y being Real st
( d = y & 0 < y ) ;
thus ((log (2,number_e)) (#) ln) . d = (log (2,number_e)) * (ln . d) by
.= (log (2,number_e)) * (log (number_e,d0)) by TAYLOR_1:def 2
.= log (2,d) by ; :: thesis: verum
end;
thus (log (2,number_e)) (#) ln is_differentiable_on right_open_halfline 0 by ; :: thesis: for x being Real st x in right_open_halfline 0 holds
( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )

thus for x being Real st x in right_open_halfline 0 holds
( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) :: thesis: verum
proof
let x be Real; :: thesis: ( x in right_open_halfline 0 implies ( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) ) )
assume A1: x in right_open_halfline 0 ; :: thesis: ( (log (2,number_e)) (#) ln is_differentiable_in x & diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )
A2: ln is_differentiable_in x by ;
hence (log (2,number_e)) (#) ln is_differentiable_in x by FDIFF_1:15; :: thesis: ( diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) / x & 0 < diff (((log (2,number_e)) (#) ln),x) )
A3: diff (ln,x) = 1 / x by ;
A4: diff (((log (2,number_e)) (#) ln),x) = (log (2,number_e)) * (diff (ln,x)) by ;
thus diff (((log (2,number_e)) (#) ln),x) = (1 * (log (2,number_e))) / x by
.= (log (2,number_e)) / x ; :: thesis: 0 < diff (((log (2,number_e)) (#) ln),x)
A5: 0 < diff (ln,x) by ;
log (2,2) < log (2,number_e) by ;
then 0 < log (2,number_e) by POWER:52;
hence 0 < diff (((log (2,number_e)) (#) ln),x) by A4, A5; :: thesis: verum
end;