let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for p, q being Point of S
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let f be PartFunc of S,T; :: thesis: for p, q being Point of S
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let p, q be Point of S; :: thesis: for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let M be Real; :: thesis: for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
let L be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); :: thesis: ( [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) implies ||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).|| )
assume that
A1: [.p,q.] c= dom f and
A2: ( ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) ) ; :: thesis: ||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||
reconsider LP = L as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
deffunc H₁( Point of S) -> Element of the carrier of T = L . ($1 - p);
consider L0 being Function of the carrier of S, the carrier of T such that
A3: for t being Element of the carrier of S holds L0 . t = H₁(t) from FUNCT_2:sch 4();
A4: dom L0 = the carrier of S by FUNCT_2:def 1;

now :: thesis: for x1, x2 being Point of S st x1 in dom L0 & x2 in dom L0 holds
||.((L0 /. x1) - (L0 /. x2)).|| <= (||.L.|| + 1) * ||.(x1 - x2).||

let x1, x2 be Point of S; :: thesis: ( x1 in dom L0 & x2 in dom L0 implies ||.((L0 /. x1) - (L0 /. x2)).|| <= (||.L.|| + 1) * ||.(x1 - x2).|| )
assume ( x1 in dom L0 & x2 in dom L0 ) ; :: thesis: ||.((L0 /. x1) - (L0 /. x2)).|| <= (||.L.|| + 1) * ||.(x1 - x2).||
( L0 /. x1 = L . (x1 - p) & L0 /. x2 = L . (x2 - p) ) by A3;
then ||.((L0 /. x1) - (L0 /. x2)).|| = ||.((LP . (x1 - p)) + ((- 1) * (LP . (x2 - p)))).|| by RLVECT_1:16
.= ||.((LP . (x1 - p)) + (LP . ((- 1) * (x2 - p)))).|| by LOPBAN_1:def 5
.= ||.(LP . ((x1 - p) + ((- 1) * (x2 - p)))).|| by VECTSP_1:def 20
.= ||.(LP . ((x1 - p) - (x2 - p))).|| by RLVECT_1:16
.= ||.(LP . (x1 - ((x2 - p) + p))).|| by RLVECT_1:27
.= ||.(LP . (x1 - (x2 - (p - p)))).|| by RLVECT_1:29
.= ||.(LP . (x1 - (x2 - (0. S)))).|| by RLVECT_1:15
.= ||.(LP . (x1 - x2)).|| by RLVECT_1:13 ;
then A5: ||.((L0 /. x1) - (L0 /. x2)).|| <= ||.L.|| * ||.(x1 - x2).|| by LOPBAN_1:32;
0 + ||.L.|| < 1 + ||.L.|| by XREAL_1:8;
then ||.L.|| * ||.(x1 - x2).|| <= (||.L.|| + 1) * ||.(x1 - x2).|| by XREAL_1:64;
hence ||.((L0 /. x1) - (L0 /. x2)).|| <= (||.L.|| + 1) * ||.(x1 - x2).|| by A5, XXREAL_0:2; :: thesis: verum

end;

then A6: L0 is_continuous_on dom L0 by NFCONT_1:45, NFCONT_1:def 9;
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
A7: dom R = the carrier of S ;

now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T ) )
assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

A8: now :: thesis: for n being Nat holds ((||.h.|| ") (#) (R /* h)) . n = 0. T

let n be Nat; :: thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T
A9: R /. (h . n) = R . (h . n) by A7, PARTFUN1:def 6
.= 0. T ;
A10: rng h c= dom R ;
A11: n in NAT by ORDINAL1:def 12;
thus ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by NDIFF_1:def 2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A11, A10, FUNCT_2:109
.= 0. T by A9, RLVECT_1:10 ; :: thesis: verum

end;

then A12: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def 18;
hence (||.h.|| ") (#) (R /* h) is convergent by NDIFF_1:18; :: thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T
((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A8;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A12, NDIFF_1:18; :: thesis: verum

end;

then reconsider R = R as RestFunc of S,T by NDIFF_1:def 5;

A13: now :: thesis: for x0 being Point of S holds
( L0 is_differentiable_in x0 & diff (L0,x0) = L )

let x0 be Point of S; :: thesis: ( L0 is_differentiable_in x0 & diff (L0,x0) = L )
set N = the Neighbourhood of x0;
A14: for x being Point of S st x in the Neighbourhood of x0 holds
(L0 /. x) - (L0 /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Point of S; :: thesis: ( x in the Neighbourhood of x0 implies (L0 /. x) - (L0 /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A15: R /. (x - x0) = R . (x - x0) by A7, PARTFUN1:def 6
.= 0. T ;
assume x in the Neighbourhood of x0 ; :: thesis: (L0 /. x) - (L0 /. x0) = (L . (x - x0)) + (R /. (x - x0))
thus (L0 /. x) - (L0 /. x0) = (L . (x - p)) - (L0 /. x0) by A3
.= (L . (x - p)) - (L . (x0 - p)) by A3
.= (LP . (x - p)) + ((- 1) * (LP . (x0 - p))) by RLVECT_1:16
.= (LP . (x - p)) + (LP . ((- 1) * (x0 - p))) by LOPBAN_1:def 5
.= LP . ((x - p) + ((- 1) * (x0 - p))) by VECTSP_1:def 20
.= LP . ((x - p) - (x0 - p)) by RLVECT_1:16
.= LP . (x - ((x0 - p) + p)) by RLVECT_1:27
.= LP . (x - (x0 - (p - p))) by RLVECT_1:29
.= LP . (x - (x0 - (0. S))) by RLVECT_1:15
.= LP . (x - x0) by RLVECT_1:13
.= (L . (x - x0)) + (R /. (x - x0)) by A15, RLVECT_1:4 ; :: thesis: verum

end;

hence L0 is_differentiable_in x0 by A4, NDIFF_1:def 6; :: thesis: diff (L0,x0) = L
hence diff (L0,x0) = L by A4, A14, NDIFF_1:def 7; :: thesis: verum

end;

set g = f - L0;
A16: dom (f - L0) = (dom f) /\ (dom L0) by VFUNCT_1:def 2
.= dom f by A4, XBOOLE_1:28 ;
A17: for x being Point of S st x in dom (f - L0) holds
(f - L0) /. x = (f /. x) - (L . (x - p))

proof

let x be Point of S; :: thesis: ( x in dom (f - L0) implies (f - L0) /. x = (f /. x) - (L . (x - p)) )
assume x in dom (f - L0) ; :: thesis: (f - L0) /. x = (f /. x) - (L . (x - p))
hence (f - L0) /. x = (f /. x) - (L0 /. x) by VFUNCT_1:def 2
.= (f /. x) - (L . (x - p)) by A3 ;
:: thesis: verum

end;

A18: for x being Point of S st x in [.p,q.] holds
f - L0 is_continuous_in x

proof

let x be Point of S; :: thesis: ( x in [.p,q.] implies f - L0 is_continuous_in x )
assume x in [.p,q.] ; :: thesis: f - L0 is_continuous_in x
then A19: f is_continuous_in x by A2;
L0 | (dom L0) is_continuous_in x by A4, A6, NFCONT_1:def 7;
hence f - L0 is_continuous_in x by A19, NFCONT_1:15; :: thesis: verum

end;

A20: for x being Point of S st x in ].p,q.[ holds
f - L0 is_differentiable_in x

proof

let x be Point of S; :: thesis: ( x in ].p,q.[ implies f - L0 is_differentiable_in x )
assume x in ].p,q.[ ; :: thesis: f - L0 is_differentiable_in x
then ( f is_differentiable_in x & L0 is_differentiable_in x ) by A2, A13;
hence f - L0 is_differentiable_in x by NDIFF_1:36; :: thesis: verum

end;

for x being Point of S st x in ].p,q.[ holds
||.(diff ((f - L0),x)).|| <= M

proof

let x be Point of S; :: thesis: ( x in ].p,q.[ implies ||.(diff ((f - L0),x)).|| <= M )
assume A21: x in ].p,q.[ ; :: thesis: ||.(diff ((f - L0),x)).|| <= M
then A22: f is_differentiable_in x by A2;
( L0 is_differentiable_in x & diff (L0,x) = L ) by A13;
then diff ((f - L0),x) = (diff (f,x)) - L by A22, NDIFF_1:36;
hence ||.(diff ((f - L0),x)).|| <= M by A2, A21; :: thesis: verum

end;

then A23: ||.(((f - L0) /. q) - ((f - L0) /. p)).|| <= M * ||.(q - p).|| by Th19, A1, A16, A18, A20;
p in [.p,q.] by RLTOPSP1:68;
then (f - L0) /. p = (f /. p) - (L . (p - p)) by A1, A16, A17;
then A24: (f - L0) /. p = (f /. p) - (LP . (0. S)) by RLVECT_1:15
.= (f /. p) - (LP . (0 * p)) by RLVECT_1:10
.= (f /. p) - (0 * (LP . p)) by LOPBAN_1:def 5
.= (f /. p) - (0. T) by RLVECT_1:10
.= f /. p by RLVECT_1:13 ;
q in [.p,q.] by RLTOPSP1:68;
then (f - L0) /. q = (f /. q) - (L . (q - p)) by A1, A16, A17;
then (f /. q) - ((L . (q - p)) + (f /. p)) = ((f - L0) /. q) - ((f - L0) /. p) by A24, RLVECT_1:27;
hence ||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).|| by A23, RLVECT_1:27; :: thesis: verum