let X, Y be RealNormSpace; :: thesis: for x being Point of X
for f being Lipschitzian LinearOperator of X,Y holds
( f is_differentiable_in x & f = diff (f,x) )
let x be Point of X; :: thesis: for f being Lipschitzian LinearOperator of X,Y holds
( f is_differentiable_in x & f = diff (f,x) )
let f be Lipschitzian LinearOperator of X,Y; :: thesis: ( f is_differentiable_in x & f = diff (f,x) )
set CX = [#] X;
A1: [#] X = dom f by FUNCT_2:def 1;
reconsider g = the carrier of X --> (0. Y) as PartFunc of X,Y ;
reconsider f0 = f as Element of BoundedLinearOperators (X,Y) by LOPBAN_1:def 9;
A2: dom g = the carrier of X ;
A3: for h being 0. X -convergent sequence of X st h is non-zero holds
( (||.h.|| ") (#) (g /* h) is convergent & lim ((||.h.|| ") (#) (g /* h)) = 0. Y )

proof

let h be 0. X -convergent sequence of X; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) (g /* h) is convergent & lim ((||.h.|| ") (#) (g /* h)) = 0. Y ) )
assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (g /* h) is convergent & lim ((||.h.|| ") (#) (g /* h)) = 0. Y )
A4: for n being Nat holds ((||.h.|| ") (#) (g /* h)) . n = 0. Y

proof

let n be Nat; :: thesis: ((||.h.|| ") (#) (g /* h)) . n = 0. Y
A5: g /. (h . n) = g . (h . n) by A2, PARTFUN1:def 6
.= 0. Y ;
A6: rng h c= dom g ;
A7: n in NAT by ORDINAL1:def 12;
thus ((||.h.|| ") (#) (g /* h)) . n = ((||.h.|| ") . n) * ((g /* h) . n) by NDIFF_1:def 2
.= ((||.h.|| ") . n) * (g /. (h . n)) by A6, A7, FUNCT_2:109
.= 0. Y by A5, RLVECT_1:10 ; :: thesis: verum

end;

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

end;

reconsider g = g as RestFunc of X,Y by A3, NDIFF_1:def 5;
ex g being Real st
( 0 < g & { y where y is Point of X : ||.(y - x).|| < g } c= [#] X ) by NDIFF_1:3;
then reconsider CX = [#] X as Neighbourhood of x by NFCONT_1:def 1;
A9: for x0 being Point of X st x0 in CX holds
(f /. x0) - (f /. x) = (f0 . (x0 - x)) + (g /. (x0 - x))

proof

let x0 be Point of X; :: thesis: ( x0 in CX implies (f /. x0) - (f /. x) = (f0 . (x0 - x)) + (g /. (x0 - x)) )
A10: g /. (x0 - x) = g . (x0 - x) by A2, PARTFUN1:def 6
.= 0. Y ;
assume x0 in CX ; :: thesis: (f /. x0) - (f /. x) = (f0 . (x0 - x)) + (g /. (x0 - x))
thus (f /. x0) - (f /. x) = (f . x0) + ((- 1) * (f . x)) by RLVECT_1:16
.= (f . x0) + (f . ((- 1) * x)) by LOPBAN_1:def 5
.= f . (x0 + ((- 1) * x)) by VECTSP_1:def 20
.= f . (x0 - x) by RLVECT_1:16
.= (f0 . (x0 - x)) + (g /. (x0 - x)) by A10, RLVECT_1:4 ; :: thesis: verum

end;

hence f is_differentiable_in x by A1; :: thesis: f = diff (f,x)
hence diff (f,x) = f by A1, A9, NDIFF_1:def 7; :: thesis: verum