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
A2: Z c= dom ((id REAL ) ^ ) ; :: thesis: ln `| Z = ((id REAL ) ^ ) | Z
A3: dom (((id REAL ) ^ ) | Z) = (dom ((id REAL ) ^ )) /\ Z by RELAT_1:90
.= Z by A2, XBOOLE_1:28 ;
A4: 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 A5: x0 in dom (((id REAL ) ^ ) | Z) ; :: thesis: (ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0
ln is_differentiable_on Z by A1, FDIFF_1:34, TAYLOR_1:18;
then (ln `| Z) . x0 = diff ln ,x0 by A3, A5, FDIFF_1:def 8
.= 1 / x0 by A1, A3, A5, 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 A2, A3, A5, RFUNCT_1:def 8
.= (((id REAL ) ^ ) | Z) . x0 by A3, A5, FUNCT_1:72 ;
hence (ln `| Z) . x0 = (((id REAL ) ^ ) | Z) . x0 ; :: thesis: verum

end;

ln is_differentiable_on Z by A1, FDIFF_1:34, TAYLOR_1:18;
then dom (((id REAL ) ^ ) | Z) = dom (ln `| Z) by A3, FDIFF_1:def 8;
hence ln `| Z = ((id REAL ) ^ ) | Z by A4, PARTFUN1:34; :: thesis: verum