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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 non-zero 0 -convergent Real_Sequence
for c being constant 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 that
A1: f is_differentiable_in x0 and
A2: diff (f,x0) = g ; :: thesis: ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant 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 ex N being Neighbourhood of x0 st N c= dom f by A1; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant 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 )
A3: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, Th11;
ex N being Neighbourhood of x0 st N c= dom f by A1;
hence for h being non-zero 0 -convergent Real_Sequence
for c being constant 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 A2, A3, Lm1; :: thesis: verum

end;

assume that
A4: ex N being Neighbourhood of x0 st N c= dom f and
A5: for h being non-zero 0 -convergent Real_Sequence
for c being constant 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 )
A6: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A5;
hence f is_differentiable_in x0 by A4, Lm1; :: thesis: diff (f,x0) = g
consider h being non-zero 0 -convergent Real_Sequence, c being constant Real_Sequence such that
A7: rng c = {x0} and
A8: rng (h + c) c= dom f and
{x0} c= dom f by A4, Th8;
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g by A5, A7, A8;
hence diff (f,x0) = g by A4, A6, A7, A8, Lm1; :: thesis: verum