let Z be open Subset of REAL; ( 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) ^)
; 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 ;
( x0 in dom (((id REAL) ^) | Z) implies (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 )
assume A5:
x0 in dom (((id REAL) ^) | Z)
;
(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
;
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; verum