let F be RealNormSpace; :: thesis: for r, p being Point of F
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
let r, p be Point of F; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + 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, the carrier of F st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + 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, the carrier of F; :: thesis: ( Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) ) )
set R = REAL --> (0. F);
defpred S₁[ object ] means $1 in REAL ;
A1: dom (REAL --> (0. F)) = REAL ;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )

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

now :: thesis: for n being Nat holds ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F

let n be Nat; :: thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) ;
A3: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def 2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by RLVECT_1:10 ; :: thesis: verum

end;

then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum

end;

then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
assume that
A4: Z c= dom f and
A5: for x being Real st x in Z holds
f /. x = (x * r) + p ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
deffunc H₁( Real) -> Element of the carrier of F = $1 * r;
consider L being PartFunc of REAL, the carrier of F such that
A6: ( ( for x being Element of REAL holds
( x in dom L iff S₁[x] ) ) & ( for x being Element of REAL st x in dom L holds
L . x = H₁(x) ) ) from SEQ_1:sch 3();
for x being Real holds
( x in dom L iff S₁[x] ) by A6;
then A7: dom L = REAL by FDIFF_1:1;
A8: for x being Element of REAL holds L /. x = H₁(x)

proof

let x be Element of REAL ; :: thesis: L /. x = H₁(x)
A9: x in dom L by A7;
L . x = H₁(x) by A6;
hence L /. x = H₁(x) by PARTFUN1:def 6, A9; :: thesis: verum

end;

A10: L is total by PARTFUN1:def 2, A7;

A11: now :: thesis: for x being Real holds L /. x = x * r

let x be Real; :: thesis: L /. x = x * r
reconsider xx = x as Element of REAL by XREAL_0:def 1;
thus L /. x = L /. xx
.= x * r by A8 ; :: thesis: verum

end;

then reconsider L = L as LinearFunc of F by A10, Def2;

A12: now :: thesis: for x0 being Real st x0 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))

proof

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A16: x - x0 in REAL by XREAL_0:def 1;
then A17: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7, A16 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A14
.= ((x * r) + p) - ((x0 * r) + p) by A5, A13
.= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27
.= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15
.= ((x - x0) * r) + (0. F) by RLVECT_1:35
.= (L /. (x - x0)) + (R /. (x - x0)) by A17, A11 ;
:: thesis: verum

end;

N c= dom f by A4, A14;
hence f is_differentiable_in x0 by A15; :: thesis: verum

end;

hence A18: f is_differentiable_on Z by A4, Th10; :: 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 A19: x0 in Z ; :: thesis: (f `| Z) . x0 = r
then consider N being Neighbourhood of x0 such that
A20: N c= Z by RCOMP_1:18;
A21: 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)) )
A22: x - x0 in REAL by XREAL_0:def 1;
then A23: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7, A22 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((x * r) + p) - (f /. x0) by A5, A20
.= ((x * r) + p) - ((x0 * r) + p) by A5, A19
.= (((x * r) + p) - (x0 * r)) - p by RLVECT_1:27
.= (p + ((x * r) - (x0 * r))) - p by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (p - p) by RLVECT_1:28
.= ((x * r) - (x0 * r)) + (0. F) by RLVECT_1:15
.= ((x - x0) * r) + (0. F) by RLVECT_1:35
.= (L /. (x - x0)) + (R /. (x - x0)) by A23, A11 ;
:: thesis: verum

end;

A24: N c= dom f by A4, A20;
A25: f is_differentiable_in x0 by A12, A19;
thus (f `| Z) . x0 = diff (f,x0) by A18, A19, Def6
.= L /. jj by A25, A24, A21, Def4
.= 1 * r by A11
.= r by RLVECT_1:def 8 ; :: thesis: verum