let r, p 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 = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
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 = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let f be PartFunc of REAL,REAL; ( Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) ) )
reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
set R = cf;
defpred S1[ set ] means $1 in REAL ;
then reconsider R = cf as RestFunc by Def2;
assume that
A7:
Z c= dom f
and
A8:
for x being Real st x in Z holds
f . x = (r * x) + p
; ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
deffunc H1( Real) -> Element of REAL = In ((r * $1),REAL);
consider L being PartFunc of REAL,REAL such that
A9:
( ( for x being Element of REAL holds
( x in dom L iff S1[x] ) ) & ( for x being Element of REAL st x in dom L holds
L . x = H1(x) ) )
from SEQ_1:sch 3();
for r being Real holds
( r in dom L iff r in REAL )
by A9;
then
dom L = REAL
by Th1;
then A10:
L is total
by PARTFUN1:def 2;
A11:
for x being Real holds L . x = r * x
then reconsider L = L as LinearFunc by A10, Def3;
hence A16:
f is_differentiable_on Z
by A7, Th9; for x being Real st x in Z holds
(f `| Z) . x = r
let x0 be Real; ( x0 in Z implies (f `| Z) . x0 = r )
assume A17:
x0 in Z
; (f `| Z) . x0 = r
then consider N being Neighbourhood of x0 such that
A18:
N c= Z
by RCOMP_1:18;
A19:
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
A20:
N c= dom f
by A7, A18;
A21:
f is_differentiable_in x0
by A12, A17;
thus (f `| Z) . x0 =
diff (f,x0)
by A16, A17, Def7
.=
L . 1
by A21, A20, A19, Def5
.=
r * 1
by A11
.=
r
; verum