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:61
.= Z by A2, XBOOLE_1:28 ;
A4: for x0 being Element of REAL st x0 in dom (((id REAL) ^) | Z) holds
(ln `| Z) . x0 = (((id REAL) ^) | Z) . x0

proof

let x0 be Element of 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:26, TAYLOR_1:18;
then (ln `| Z) . x0 = diff (ln,x0) by A3, A5, FDIFF_1:def 7
.= 1 / x0 by A1, A3, A5, TAYLOR_1:18
.= 1 / ((id REAL) . x0)
.= 1 * (((id REAL) . x0) ") by XCMPLX_0:def 9
.= 1 * (((id REAL) ^) . x0) by A2, A3, A5, RFUNCT_1:def 2
.= (((id REAL) ^) | Z) . x0 by A3, A5, FUNCT_1:49 ;
hence (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 ; :: thesis: verum

end;

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