:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :
for S, T being RealNormSpace
for f being PartFunc of S,T
for x0, z being Point of S st f is_Gateaux_differentiable_in x0,z holds
for b₆ being Point of T holds
( b₆ = Gateaux_diff (f,x0,z) iff ex N being Neighbourhood of x0 st
( N c= dom f & ( 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))) - b₆).|| < e ) ) ) ) );