let r, p be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 S_{1}[ set ] means $1 in REAL ;

assume that

A7: Z c= dom f and

A8: for x being Real st x in Z holds

f . x = (r * x) + p ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

deffunc H_{1}( 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 S_{1}[x] ) ) & ( for x being Element of REAL st x in dom L holds

L . x = H_{1}(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

(f `| Z) . x = r

let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = r )

assume A17: x0 in Z ; :: thesis: (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))

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 ; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 S

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

then reconsider R = cf as RestFunc by Def2;( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

hence (h ") (#) (cf /* h) is convergent ; :: thesis: lim ((h ") (#) (cf /* h)) = 0

((h ") (#) (cf /* h)) . 0 = 0 by A2;

hence lim ((h ") (#) (cf /* h)) = 0 by A6, SEQ_4:25; :: thesis: verum

end;A2: now :: thesis: for n being Nat holds ((h ") (#) (cf /* h)) . n = 0

then A6:
(h ") (#) (cf /* h) is V8()
by VALUED_0:def 18;let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0

A3: rng h c= dom cf ;

A5: n in NAT by ORDINAL1:def 12;

thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8

.= ((h ") . n) * (cf . (h . n)) by A5, A3, FUNCT_2:108

.= ((h ") . n) * 0

.= 0 ; :: thesis: verum

end;A3: rng h c= dom cf ;

A5: n in NAT by ORDINAL1:def 12;

thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8

.= ((h ") . n) * (cf . (h . n)) by A5, A3, FUNCT_2:108

.= ((h ") . n) * 0

.= 0 ; :: thesis: verum

hence (h ") (#) (cf /* h) is convergent ; :: thesis: lim ((h ") (#) (cf /* h)) = 0

((h ") (#) (cf /* h)) . 0 = 0 by A2;

hence lim ((h ") (#) (cf /* h)) = 0 by A6, SEQ_4:25; :: thesis: verum

assume that

A7: Z c= dom f and

A8: for x being Real st x in Z holds

f . x = (r * x) + p ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = r ) )

deffunc H

consider L being PartFunc of REAL,REAL such that

A9: ( ( for x being Element of REAL holds

( x in dom L iff S

L . x = H

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

proof

then reconsider L = L as LinearFunc by A10, Def3;
let x be Real; :: thesis: L . x = r * x

reconsider x = x as Element of REAL by XREAL_0:def 1;

L . x = H_{1}(x)
by A9;

hence L . x = r * x ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

L . x = H

hence L . x = r * x ; :: thesis: verum

A12: now :: thesis: for x0 being Real st x0 in Z holds

f is_differentiable_in x0

hence A16:
f is_differentiable_on Z
by A7, Th9; :: thesis: for x being Real st x in Z holds f is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )

assume A13: x0 in Z ; :: thesis: f is_differentiable_in x0

then consider N being Neighbourhood of x0 such that

A14: N c= Z by RCOMP_1:18;

A15: for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

hence f is_differentiable_in x0 by A15; :: thesis: verum

end;assume A13: x0 in Z ; :: thesis: f is_differentiable_in x0

then consider N being Neighbourhood of x0 such that

A14: N c= Z by RCOMP_1:18;

A15: for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

N c= dom f
by A7, A14;
let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A8, A14

.= ((r * x) + p) - ((r * x0) + p) by A8, A13

.= (r * (x - x0)) + 0

.= (L . (xx - xx0)) + 0 by A11

.= (L . (x - x0)) + (R . (x - x0)) ;

:: thesis: verum

end;reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A8, A14

.= ((r * x) + p) - ((r * x0) + p) by A8, A13

.= (r * (x - x0)) + 0

.= (L . (xx - xx0)) + 0 by A11

.= (L . (x - x0)) + (R . (x - x0)) ;

:: thesis: verum

hence f is_differentiable_in x0 by A15; :: thesis: verum

(f `| Z) . x = r

let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = r )

assume A17: x0 in Z ; :: thesis: (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))

proof

A20:
N c= dom f
by A7, A18;
let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )

reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A8, A18

.= ((r * x) + p) - ((r * x0) + p) by A8, A17

.= (r * (x - x0)) + 0

.= (L . (xx - xx0)) + 0 by A11

.= (L . (x - x0)) + (R . (x - x0)) ;

:: thesis: verum

end;reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x in N ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

hence (f . x) - (f . x0) = ((r * x) + p) - (f . x0) by A8, A18

.= ((r * x) + p) - ((r * x0) + p) by A8, A17

.= (r * (x - x0)) + 0

.= (L . (xx - xx0)) + 0 by A11

.= (L . (x - x0)) + (R . (x - x0)) ;

:: thesis: verum

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 ; :: thesis: verum