let a be Real; for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
let f be PartFunc of REAL,REAL; ( Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) implies ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) )
assume that
A1:
Z c= dom (2 (#) ((#R (1 / 2)) * f))
and
A2:
for x being Real st x in Z holds
( f . x = a + x & f . x > 0 )
; ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
A3:
Z c= dom ((#R (1 / 2)) * f)
by A1, VALUED_1:def 5;
then
for y being object st y in Z holds
y in dom f
by FUNCT_1:11;
then A4:
Z c= dom f
by TARSKI:def 3;
A5:
for x being Real st x in Z holds
f . x = (1 * x) + a
by A2;
then A6:
f is_differentiable_on Z
by A4, FDIFF_1:23;
then A7:
(#R (1 / 2)) * f is_differentiable_on Z
by A3, FDIFF_1:9;
for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2))
proof
let x be
Real;
( x in Z implies ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) )
assume A8:
x in Z
;
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2))
then A9:
f . x = a + x
by A2;
A10:
(
f is_differentiable_in x &
f . x > 0 )
by A2, A6, A8, FDIFF_1:9;
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x =
2
* (diff (((#R (1 / 2)) * f),x))
by A1, A7, A8, FDIFF_1:20
.=
2
* (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x)))
by A10, TAYLOR_1:22
.=
2
* (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x))
by A6, A8, FDIFF_1:def 7
.=
2
* (((1 / 2) * ((a + x) #R ((1 / 2) - 1))) * 1)
by A4, A5, A8, A9, FDIFF_1:23
.=
(a + x) #R (- (1 / 2))
;
hence
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2))
;
verum
end;
hence
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
by A1, A7, FDIFF_1:20; verum