let Z be open Subset of REAL ; :: thesis: ( Z c= dom ln & Z c= dom ((id REAL ) ^ ) implies ln `| Z = ((id REAL ) ^ ) | Z )
assume that
A1: Z c= dom ln and
A: Z c= dom ((id REAL ) ^ ) ; :: thesis: ln `| Z = ((id REAL ) ^ ) | Z
AA: dom (((id REAL ) ^ ) | Z) = (dom ((id REAL ) ^ )) /\ Z by RELAT_1:90
.= Z by A, XBOOLE_1:28 ;
ln is_differentiable_on Z by A1, FDIFF_1:34, TAYLOR_1:18;
then B: dom (((id REAL ) ^ ) | Z) = dom (ln `| Z) by AA, FDIFF_1:def 8;
for x0 being Real st x0 in dom (((id REAL ) ^ ) | Z) holds
(ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0

proof

let x0 be Real; :: thesis: ( x0 in dom (((id REAL ) ^ ) | Z) implies (ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0 )
assume A3: x0 in dom (((id REAL ) ^ ) | Z) ; :: thesis: (ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0
A5: ln is_differentiable_on Z by A1, FDIFF_1:34, TAYLOR_1:18;
(ln `| Z) . x0 = diff ln ,x0 by AA, A3, A5, FDIFF_1:def 8
.= 1 / x0 by A1, AA, A3, TAYLOR_1:18
.= 1 / ((id REAL ) . x0) by FUNCT_1:35
.= 1 * (((id REAL ) . x0) " ) by XCMPLX_0:def 9
.= 1 * (((id REAL ) ^ ) . x0) by A, AA, A3, RFUNCT_1:def 8
.= (((id REAL ) ^ ) | Z) . x0 by AA, A3, FUNCT_1:72 ;
hence (ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0 ; :: thesis: verum

end;

hence ln `| Z = ((id REAL ) ^ ) | Z by B, PARTFUN1:34; :: thesis: verum