let Z be open Subset of REAL ; :: thesis: ( Z c= dom (ln * ln ) & ( 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
((ln * ln ) `| Z) . x = 1 / ((ln . x) * x) ) ) )
assume that
A1: Z c= dom (ln * ln ) 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
((ln * ln ) `| 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: ln . x > 0
then A4: ln . x in right_open_halfline 0 by A1, FUNCT_1:21, TAYLOR_1:18;
].0 ,+infty .[ = { 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 is_differentiable_in x by A2, TAYLOR_1:18;
A6: for x being Real st x in Z holds
ln * ln is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ln * ln is_differentiable_in x )
assume A7: x in Z ; :: thesis: ln * ln is_differentiable_in x
then A8: ln is_differentiable_in x by A5;
( x > 0 & ln . x > 0 ) by A2, A3, A7;
hence ln * ln is_differentiable_in x by A8, TAYLOR_1:20; :: thesis: verum

end;

then A9: ln * ln is_differentiable_on Z by A1, FDIFF_1:16;
for x being Real st x in Z holds
((ln * ln ) `| Z) . x = 1 / ((ln . x) * x)

proof

let x be Real; :: thesis: ( x in Z implies ((ln * ln ) `| Z) . x = 1 / ((ln . x) * x) )
assume A10: x in Z ; :: thesis: ((ln * ln ) `| Z) . x = 1 / ((ln . x) * x)
then A11: ln is_differentiable_in x by A5;
A12: ( x > 0 & ln . x > 0 ) by A2, A3, A10;
].0 ,+infty .[ = { g where g is Real : 0 < g } by XXREAL_1:230;
then A13: x in right_open_halfline 0 by A12;
diff (ln * ln ),x = (diff ln ,x) / (ln . x) by A11, A12, TAYLOR_1:20
.= (1 / (ln . x)) * (1 / x) by A13, TAYLOR_1:18
.= 1 / ((ln . x) * x) by XCMPLX_1:103 ;
hence ((ln * ln ) `| Z) . x = 1 / ((ln . x) * x) by A9, A10, FDIFF_1:def 8; :: thesis: verum

end;

hence ( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * ln ) `| Z) . x = 1 / ((ln . x) * x) ) ) by A1, A6, FDIFF_1:16; :: thesis: verum