let Z be open Subset of REAL ; ( not 0 in Z implies ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^ ) `| Z) . x = - (1 / (x ^2 )) ) ) )
set f = id Z;
A1:
( Z c= dom (id Z) & ( for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 ) )
by FUNCT_1:34, FUNCT_1:35;
then A2:
id Z is_differentiable_on Z
by FDIFF_1:31;
assume A3:
not 0 in Z
; ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^ ) `| Z) . x = - (1 / (x ^2 )) ) )
then A4:
for x being Real st x in Z holds
(id Z) . x <> 0
by FUNCT_1:35;
then A5:
(id Z) ^ is_differentiable_on Z
by A2, FDIFF_2:22;
now let x be
Real;
( x in Z implies (((id Z) ^ ) `| Z) . x = - (1 / (x ^2 )) )assume A6:
x in Z
;
(((id Z) ^ ) `| Z) . x = - (1 / (x ^2 ))then A7:
(
(id Z) . x <> 0 &
id Z is_differentiable_in x )
by A3, A2, FDIFF_1:16, FUNCT_1:35;
(((id Z) ^ ) `| Z) . x =
diff ((id Z) ^ ),
x
by A5, A6, FDIFF_1:def 8
.=
- ((diff (id Z),x) / (((id Z) . x) ^2 ))
by A7, FDIFF_2:15
.=
- ((((id Z) `| Z) . x) / (((id Z) . x) ^2 ))
by A2, A6, FDIFF_1:def 8
.=
- (1 / (((id Z) . x) ^2 ))
by A1, A6, FDIFF_1:31
.=
- (1 / (x ^2 ))
by A6, FUNCT_1:35
;
hence
(((id Z) ^ ) `| Z) . x = - (1 / (x ^2 ))
;
verum end;
hence
( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) ^ ) `| Z) . x = - (1 / (x ^2 )) ) )
by A2, A4, FDIFF_2:22; verum