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

proof

let x0 be Real; :: thesis: ( x0 in dom (((#Z 1) ^ ) | Z) implies (ln `| Z) . x0 = (((#Z 1) ^ ) | Z) . x0 )
assume A3: x0 in dom (((#Z 1) ^ ) | Z) ; :: thesis: (ln `| Z) . x0 = (((#Z 1) ^ ) | 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 / (x0 #Z 1) by PREPOWER:45
.= 1 / ((#Z 1) . x0) by TAYLOR_1:def 1
.= 1 * (((#Z 1) . x0) " ) by XCMPLX_0:def 9
.= 1 * (((#Z 1) ^ ) . x0) by A, AA, A3, RFUNCT_1:def 8
.= (((#Z 1) ^ ) | Z) . x0 by AA, A3, FUNCT_1:72 ;
hence (ln `| Z) . x0 = (((#Z 1) ^ ) | Z) . x0 ; :: thesis: verum

end;

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