let S, T be RealNormSpace; :: thesis:
let L0 be Lipschitzian LinearOperator of S,T; :: thesis:
let x0 be Point of S; :: thesis:
the carrier of S c= the carrier of S ;
then reconsider Z = the carrier of S as Subset of S ;
reconsider E = {} as Subset of S by XBOOLE_1:2;
reconsider L = L0 as Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) by LOPBAN_1:def 9;
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
A6: dom R = the carrier of S ;

now :: thesis:

let h be 0. S -convergent sequence of S; :: thesis:
assume h is non-zero ; :: thesis:

A7: now :: thesis:

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

end;

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

end;

then reconsider R = R as RestFunc of S,T by NDIFF_1:def 5;
set N = the Neighbourhood of x0;
A15: 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:
A16: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def 6
.= 0. T ;
assume x in the Neighbourhood of x0 ; :: thesis:
thus (L0 /. x) - (L0 /. x0) = L . (x - x0) by LM001
.= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ; :: thesis:

end;

A17: dom L0 = the carrier of S by FUNCT_2:def 1;
hence L0 is_differentiable_in x0 by A15; :: thesis:
hence diff (L0,x0) = L0 by A17, A15, NDIFF_1:def 7; :: thesis: