let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds
for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) ) )
assume f is_differentiable_in x0 ; :: thesis: for z being Point of S holds
( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: for z being Point of S
for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by Th1;
let z be Point of S; :: thesis: ( f is_Gateaux_differentiable_in x0,z & Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
A3: for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & (diff (f,x0)) . z = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) by A2;
then A4: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d & h <> 0 & (h * z) + x0 in N holds
||.(((h ") * ((f /. ((h * z) + x0)) - (f /. x0))) - ((diff (f,x0)) . z)).|| < e ) ) by A1, Th3;
hence f is_Gateaux_differentiable_in x0,z by A1; :: thesis: ( Gateaux_diff (f,x0,z) = (diff (f,x0)) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) )
hence Gateaux_diff (f,x0,z) = (diff (f,x0)) . z by A1, A4, Def4; :: 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 sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
hence ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence
for c being constant sequence of S st rng c = {x0} & rng ((h * z) + c) c= N holds
( (h ") (#) ((f /* ((h * z) + c)) - (f /* c)) is convergent & Gateaux_diff (f,x0,z) = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) by A1, A3; :: thesis: verum