let S, T be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of S,T
for x0 being Point of S holds
( L is_differentiable_in x0 & diff (L,x0) = L )
let L0 be Lipschitzian LinearOperator of S,T; :: thesis: for x0 being Point of S holds
( L0 is_differentiable_in x0 & diff (L0,x0) = L0 )
let x0 be Point of S; :: thesis: ( L0 is_differentiable_in x0 & diff (L0,x0) = L0 )
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: 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 )

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

let n be Nat; :: thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T
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: verum

end;

then A11: (||.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 A7;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A11, NDIFF_1:18; :: thesis: verum

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: ( x in the Neighbourhood of x0 implies (L0 /. x) - (L0 /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A16: R /. (x - x0) = R . (x - x0) by A6, 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 - x0) by LM001
.= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ; :: thesis: verum

end;

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