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 8;
A3:
dom ((#Z 2) ^ ) = REAL \ {0 }
by Th3;
then A4:
Z c= dom ((#Z 2) ^ )
by A1, ZFMISC_1:40;
A5:
for x0 being 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
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 8
.=
- (1 / (x0 ^2 ))
by A1, A7, Th45
.=
- (1 / (x0 |^ (1 + 1)))
by NEWTON:100
.=
- (1 / (x0 #Z 2))
by PREPOWER:46
.=
- (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 8
.=
(- 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:72
;
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:90
.=
(dom ((#Z 2) ^ )) /\ Z
by VALUED_1:def 5
.=
Z
by A1, A3, XBOOLE_1:28, ZFMISC_1:40
;
hence
((id REAL ) ^ ) `| Z = ((- 1) (#) ((#Z 2) ^ )) | Z
by A2, A5, PARTFUN1:34; verum