let T, S be non trivial 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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 A1: 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 convergent_to_0 Real_Sequence
for c being V8() 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 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 convergent_to_0 Real_Sequence
for c being V8() 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))) ) ) ) )
consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: for z being Point of S
for h being convergent_to_0 Real_Sequence
for c being V8() 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 A1, Th1;
A4: for h being convergent_to_0 Real_Sequence
for c being V8() 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 A3;
then A5: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st abs h < d & h <> 0 & (h * z) + x0 in N holds
||.(((h " ) * ((f /. ((h * z) + x0)) - (f /. x0))) - ((diff f,x0) . z)).|| < e ) ) by A2, Th3;
hence f is_Gateaux_differentiable_in x0,z by A2, Def3; :: thesis: ( Gateaux_diff f,x0,z = (diff f,x0) . z & ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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 A2, A5, Def4; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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 convergent_to_0 Real_Sequence
for c being V8() 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 A2, A4; :: thesis: verum