let x0, g be Real; :: thesis: for f being PartFunc of REAL ,REAL holds
( f is_differentiable_in x0 & diff f,x0 = g iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 & diff f,x0 = g iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) )
thus ( f is_differentiable_in x0 & diff f,x0 = g implies ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) ) :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) implies ( f is_differentiable_in x0 & diff f,x0 = g ) )

proof

assume A1: ( f is_differentiable_in x0 & diff f,x0 = g ) ; :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) )
then A2: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) by Th11;
thus ex N being Neighbourhood of x0 st N c= dom f by A1, Th11; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g )
thus for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) by A1, A2, Lm1; :: thesis: verum

end;

assume A3: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) ; :: thesis: ( f is_differentiable_in x0 & diff f,x0 = g )
then A4: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent ;
hence f is_differentiable_in x0 by A3, Lm1; :: thesis: diff f,x0 = g
consider h being convergent_to_0 Real_Sequence, c being V8() Real_Sequence such that
A5: ( rng c = {x0} & rng (h + c) c= dom f & {x0} c= dom f ) by A3, Th8;
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g by A3, A5;
hence diff f,x0 = g by A3, A4, A5, Lm1; :: thesis: verum