let Z be open Subset of REAL; :: thesis: ( Z c= dom () & ( for x being Real st x in Z holds
x > 0 ) implies ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = 1 / ((ln . x) * x) ) ) )

assume that
A1: Z c= dom () and
A2: for x being Real st x in Z holds
x > 0 ; :: thesis: ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = 1 / ((ln . x) * x) ) )

A3: for x being Real st x in Z holds
ln . x > 0
proof
let x be Real; :: thesis: ( x in Z implies ln . x > 0 )
assume x in Z ; :: thesis:
then A4: ln . x in right_open_halfline 0 by ;
]..[ = { g where g is Real : 0 < g } by XXREAL_1:230;
then ex g being Real st
( ln . x = g & 0 < g ) by A4;
hence ln . x > 0 ; :: thesis: verum
end;
A5: for x being Real st x in Z holds
ln * ln is_differentiable_in x
proof end;
then A8: ln * ln is_differentiable_on Z by ;
for x being Real st x in Z holds
(() `| Z) . x = 1 / ((ln . x) * x)
proof
let x be Real; :: thesis: ( x in Z implies (() `| Z) . x = 1 / ((ln . x) * x) )
A9: ]..[ = { g where g is Real : 0 < g } by XXREAL_1:230;
assume A10: x in Z ; :: thesis: (() `| Z) . x = 1 / ((ln . x) * x)
then A11: ln . x > 0 by A3;
x > 0 by ;
then A12: x in right_open_halfline 0 by A9;
ln is_differentiable_in x by ;
then diff ((),x) = (diff (ln,x)) / (ln . x) by
.= (1 / (ln . x)) * (1 / x) by
.= 1 / ((ln . x) * x) by XCMPLX_1:102 ;
hence ((ln * ln) `| Z) . x = 1 / ((ln . x) * x) by ; :: thesis: verum
end;
hence ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = 1 / ((ln . x) * x) ) ) by ; :: thesis: verum