let a be Real; for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) )
let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) )
let f be PartFunc of REAL,REAL; ( Z c= dom f & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) implies ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) )
assume that
A1:
Z c= dom f
and
A2:
for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 )
; ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) )
A3:
for x being Real st x in Z holds
f . x = (1 * x) + a
by A2;
then A4:
f is_differentiable_on Z
by A1, FDIFF_1:23;
A5:
for x being Real st x in Z holds
f . x <> 0
by A2;
then A6:
f ^ is_differentiable_on Z
by A4, FDIFF_2:22;
now for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2))let x be
Real;
( x in Z implies ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) )assume A7:
x in Z
;
((f ^) `| Z) . x = - (1 / ((a + x) ^2))then A8:
(
f . x <> 0 &
f is_differentiable_in x )
by A2, A4, FDIFF_1:9;
((f ^) `| Z) . x =
diff (
(f ^),
x)
by A6, A7, FDIFF_1:def 7
.=
- ((diff (f,x)) / ((f . x) ^2))
by A8, FDIFF_2:15
.=
- (((f `| Z) . x) / ((f . x) ^2))
by A4, A7, FDIFF_1:def 7
.=
- (1 / ((f . x) ^2))
by A1, A3, A7, FDIFF_1:23
.=
- (1 / ((a + x) ^2))
by A2, A7
;
hence
((f ^) `| Z) . x = - (1 / ((a + x) ^2))
;
verum end;
hence
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) )
by A4, A5, FDIFF_2:22; verum