let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds
f . x = x - 1 ) holds
( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) )
let f be PartFunc of REAL,REAL; ( Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds
f . x = x - 1 ) implies ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) )
assume that
A1:
Z c= dom (exp_R (#) f)
and
A2:
for x being Real st x in Z holds
f . x = x - 1
; ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) )
A3:
for x being Real st x in Z holds
f . x = (1 * x) + (- 1)
proof
let x be
Real;
( x in Z implies f . x = (1 * x) + (- 1) )
A4:
(1 * x) + (- 1) = (1 * x) - 1
;
assume
x in Z
;
f . x = (1 * x) + (- 1)
hence
f . x = (1 * x) + (- 1)
by A2, A4;
verum
end;
Z c= (dom f) /\ (dom exp_R)
by A1, VALUED_1:def 4;
then A5:
Z c= dom f
by XBOOLE_1:18;
then A6:
f is_differentiable_on Z
by A3, FDIFF_1:23;
A7:
exp_R is_differentiable_on Z
by FDIFF_1:26, TAYLOR_1:16;
now for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x)let x be
Real;
( x in Z implies ((exp_R (#) f) `| Z) . x = x * (exp_R . x) )assume A8:
x in Z
;
((exp_R (#) f) `| Z) . x = x * (exp_R . x)hence ((exp_R (#) f) `| Z) . x =
((f . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (f,x)))
by A1, A6, A7, FDIFF_1:21
.=
((x - 1) * (diff (exp_R,x))) + ((exp_R . x) * (diff (f,x)))
by A2, A8
.=
((x - 1) * (exp_R . x)) + ((exp_R . x) * (diff (f,x)))
by TAYLOR_1:16
.=
((x - 1) * (exp_R . x)) + ((exp_R . x) * ((f `| Z) . x))
by A6, A8, FDIFF_1:def 7
.=
((x - 1) * (exp_R . x)) + ((exp_R . x) * 1)
by A5, A3, A8, FDIFF_1:23
.=
x * (exp_R . x)
;
verum end;
hence
( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) )
by A1, A6, A7, FDIFF_1:21; verum