let S, T be 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 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 & 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 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 & 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 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 & dv = lim ((h ") (#) ((f /* ((h * z) + c)) - (f /* c))) ) ) )

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

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

end;

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

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