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

(ln `| Z) . x = 1 / x ) ) by A1, A2, FDIFF_1:9; :: thesis: verum

(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

hence
( ln is_differentiable_on Z & ( for x being Real st x in Z holds
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;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

(ln `| Z) . x = 1 / x ) ) by A1, A2, FDIFF_1:9; :: thesis: verum