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
proof
let x be
Real;
( x in Z implies f . x = ((- 1) * x) + a )
assume
x in Z
;
f . x = ((- 1) * x) + a
then
f . x = a - x
by A2;
hence
f . x = ((- 1) * x) + a
;
verum
end;
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 / ((f . x) ^2)))
by XCMPLX_1:187
.=
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