let Z be open Subset of REAL ; :: thesis: ( Z c= dom ln implies ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) ) )
assume A1: Z c= dom ln ; :: thesis: ( ln is_differentiable_on Z & ( for x being Real st x in Z holds
(ln `| Z) . x = 1 / x ) )
A5: for x being Real st x in Z holds
ln is_differentiable_in x by Lem10, A1, TAYLOR_1:18;
then A8: ln is_differentiable_on Z by A1, FDIFF_1:16;
for x being Real st x in Z holds
(ln `| Z) . x = 1 / x

proof

let x be Real; :: thesis: ( x in Z implies (ln `| Z) . x = 1 / x )
assume A9: x in Z ; :: thesis: (ln `| Z) . x = 1 / x
then x in right_open_halfline 0 by A1, TAYLOR_1:18;
then diff ln ,x = 1 / x by TAYLOR_1:18;
hence (ln `| Z) . x = 1 / x by A8, A9, FDIFF_1:def 8; :: thesis: verum

end;

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