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 ) ) )
assume A1: ( Z c= dom f & ( 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 ) )
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = r * $1;
consider L being PartFunc of REAL ,REAL such that
A2: ( ( for x being Real holds
( x in dom L iff S₁[x] ) ) & ( for x being Real st x in dom L holds
L . x = H₁(x) ) ) from SEQ_1:sch 3();
dom L = REAL by A2, Th1;
then A3: L is total by PARTFUN1:def 4;

A4: now

let x be Real; :: thesis: L . x = r * x
x in dom L by A2;
hence L . x = r * x by A2; :: thesis: verum

end;

then reconsider L = L as LINEAR by A3, Def4;
set R = cf;
A5: dom cf = REAL by FUNCOP_1:19;

now

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

A6: now

let n be Nat; :: thesis: ((h " ) (#) (cf /* h)) . n = 0
X: n in NAT by ORDINAL1:def 13;
A7: rng h c= dom cf by A5;
thus ((h " ) (#) (cf /* h)) . n = ((h " ) . n) * ((cf /* h) . n) by X, SEQ_1:12
.= ((h " ) . n) * (cf . (h . n)) by A7, X, FUNCT_2:185
.= ((h " ) . n) * 0 by FUNCOP_1:13
.= 0 ; :: thesis: verum

end;

then A8: (h " ) (#) (cf /* h) is V8() by VALUED_0:def 18;
hence (h " ) (#) (cf /* h) is convergent ; :: thesis: lim ((h " ) (#) (cf /* h)) = 0
((h " ) (#) (cf /* h)) . 0 = 0 by A6;
hence lim ((h " ) (#) (cf /* h)) = 0 by A8, SEQ_4:40; :: thesis: verum

end;

then reconsider R = cf as REST by Def3;

A9: now

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A10: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A11: N c= Z by RCOMP_1:39;
A12: N c= dom f by A1, A11, XBOOLE_1:1;
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
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 A1, A11
.= ((r * x) + p) - ((r * x0) + p) by A1, A10
.= (r * (x - x0)) + 0
.= (L . (x - x0)) + 0 by A4
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A12, Def5; :: thesis: verum

end;

hence A13: f is_differentiable_on Z by A1, Th16; :: thesis: for x being Real st x in Z holds
(f `| Z) . x = r
let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) . x0 = r )
assume A14: x0 in Z ; :: thesis: (f `| Z) . x0 = r
then A15: f is_differentiable_in x0 by A9;
consider N being Neighbourhood of x0 such that
A16: N c= Z by A14, RCOMP_1:39;
A17: N c= dom f by A1, A16, XBOOLE_1:1;
A18: for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
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 A1, A16
.= ((r * x) + p) - ((r * x0) + p) by A1, A14
.= (r * (x - x0)) + 0
.= (L . (x - x0)) + 0 by A4
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:13 ;
:: thesis: verum

end;

thus (f `| Z) . x0 = diff f,x0 by A13, A14, Def8
.= L . 1 by A15, A17, A18, Def6
.= r * 1 by A4
.= r ; :: thesis: verum