let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
let f be PartFunc of S,T; :: thesis: for x0, z being Point of S holds
( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )
let x0, z be Point of S; :: thesis: ( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )

A1: now

assume f is_Gateaux_differentiable_in x0,z ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) )
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: 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))) - (Gateaux_diff f,x0,z)).|| < e ) ) by Def4;
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, A3, Th3;
hence ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) by A2; :: thesis: verum

end;

now

assume ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ; :: thesis: f is_Gateaux_differentiable_in x0,z
then consider N being Neighbourhood of x0 such that
A4: N c= dom f and
A5: ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ;
consider dv being Point of T such that
A6: 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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) by 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))) - dv).|| < e ) ) by A4, A6, Th3;
hence f is_Gateaux_differentiable_in x0,z by A4, Def3; :: thesis: verum

end;

hence ( f is_Gateaux_differentiable_in x0,z iff ex N being Neighbourhood of x0 st
( N c= dom f & ex dv being Point of T st
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 & dv = lim ((h " ) (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) ) by A1; :: thesis: verum