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 ) )
then A2: for x being Real st x in Z holds
ln is_differentiable_in x by Lm5, TAYLOR_1:18;
then A3: ln is_differentiable_on Z by A1, FDIFF_1:9;
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 A4: x in Z ; :: thesis: (ln `| Z) . x = 1 / x
then diff (ln,x) = 1 / x by A1, TAYLOR_1:18;
hence (ln `| Z) . x = 1 / x by A3, A4, FDIFF_1:def 7; :: 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, A2, FDIFF_1:9; :: thesis: verum