let Z be open Subset of REAL; ( not 0 in Z implies ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z )
assume A1:
not 0 in Z
; ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z
then
(id REAL) ^ is_differentiable_on Z
by Lm2, Th43;
then A2:
dom (((id REAL) ^) `| Z) = Z
by FDIFF_1:def 7;
A3:
dom ((#Z 2) ^) = REAL \ {0}
by Th3;
then A4:
Z c= dom ((#Z 2) ^)
by A1, ZFMISC_1:34;
A5:
for x0 being Element of REAL st x0 in Z holds
(((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0
proof
A6:
dom ((- 1) (#) ((#Z 2) ^)) = dom ((#Z (1 + 1)) ^)
by VALUED_1:def 5;
let x0 be
Element of
REAL ;
( x0 in Z implies (((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0 )
assume A7:
x0 in Z
;
(((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0
(id REAL) ^ is_differentiable_on Z
by A1, Lm2, Th43;
then (((id REAL) ^) `| Z) . x0 =
diff (
((id REAL) ^),
x0)
by A7, FDIFF_1:def 7
.=
- (1 / (x0 ^2))
by A1, A7, Th45
.=
- (1 / (x0 |^ (1 + 1)))
by NEWTON:81
.=
- (1 / (x0 #Z 2))
by PREPOWER:36
.=
- (1 / ((#Z 2) . x0))
by TAYLOR_1:def 1
.=
- (1 * (((#Z 2) . x0) "))
by XCMPLX_0:def 9
.=
- (1 * (((#Z 2) ^) . x0))
by A4, A7, RFUNCT_1:def 2
.=
(- 1) * (((#Z 2) ^) . x0)
.=
((- 1) (#) ((#Z 2) ^)) . x0
by A4, A7, A6, VALUED_1:def 5
.=
(((- 1) (#) ((#Z 2) ^)) | Z) . x0
by A7, FUNCT_1:49
;
hence
(((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0
;
verum
end;
dom (((- 1) (#) ((#Z (1 + 1)) ^)) | Z) =
(dom ((- 1) (#) ((#Z 2) ^))) /\ Z
by RELAT_1:61
.=
(dom ((#Z 2) ^)) /\ Z
by VALUED_1:def 5
.=
Z
by A1, A3, XBOOLE_1:28, ZFMISC_1:34
;
hence
((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z
by A2, A5, PARTFUN1:5; verum