0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & h*z+x0 in N holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv .|| < e ) proof let x0 be Point of S; let N be Neighbourhood of x0 such that A1: N c= dom f; let z be Point of S; let dv be Point of T; A2: now reconsider c = NAT --> x0 as sequence of S; assume A3: for h be 0-convergent non-zero Real_Sequence for c 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)); now let x be object; assume x in {x0}; then x=x0 by TARSKI:def 1; then x=c.1 by FUNCOP_1:7; hence x in rng c by NFCONT_1:6; end; then A4: {x0} c= rng c; now let x be object; assume x in rng c; then consider n be Nat such that A5: x=c.n by NFCONT_1:6; n in NAT by ORDINAL1:def 12; then x=x0 by FUNCOP_1:7,A5; hence x in {x0} by TARSKI:def 1; end; then rng c c= {x0}; then A6: rng c = {x0} by A4,XBOOLE_0:def 10; assume not ( for r be Real st r > 0 holds ex d be Real st d > 0 & for h be Real st |.h.| < d & h <> 0 & h*z+x0 in N holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv .|| < r ); then consider r be Real such that A7: r > 0 and A8: for d be Real st d > 0 holds ex h be Real st |.h.| < d & h <> 0 & h*z+x0 in N & not ||. h"*(f/.(h*z+x0) - f/.x0) - dv .|| < r; defpred P[Nat,Real] means ex rr being Real st rr = $2 & |.rr.| < ( 1/($1+1)) & rr <> 0 & rr*z+x0 in N & not ( ||. rr"*(f/.(rr*z+x0) - f/.x0) - dv .|| < r ); A9: for n be Element of NAT ex h be Element of REAL st P[n,h] proof let n be Element of NAT; 0 < 1 * (n + 1)"; then 0 < 1/(n + 1) by XCMPLX_0:def 9; then consider h be Real such that A10: |.h.| < 1/(n + 1) & h <> 0 & h*z+x0 in N & not ||. h"*(f/.(h*z+x0) - f/.x0) - dv .|| < r by A8; h in REAL by XREAL_0:def 1; hence thesis by A10; end; consider h be Real_Sequence such that A11: for n be Element of NAT holds P[n,h.n] from FUNCT_2:sch 3(A9); A12: now let p be Real; assume A13: 0

0
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then P[n,h.n] by A11;
hence thesis;
end;
then h is non-zero by SEQ_1:5;
then reconsider h as 0-convergent non-zero Real_Sequence
by A18,A19,FDIFF_1:def 1;
now
let x be object;
assume x in rng (h*z+c);
then consider n be Nat such that
A20: x=(h*z+c).n by NFCONT_1:6;
A21: n in NAT by ORDINAL1:def 12;
A22: x=(h*z).n+c.n by A20,NORMSP_1:def 2
.=(h.n)*z+c.n by NDIFF_1:def 3
.=(h.n)*z+x0 by FUNCOP_1:7,A21;
P[n,h.n] by A11,A21;
hence x in N by A22;
end;
then
A23: rng (h*z+c) c= N;
then
h"(#)(f/*(h*z+c) - f/*c) is convergent & dv = lim (h"(#)(f/*(h*z+c) -
f/*c)) by A3,A6;
then consider n be Nat such that
A24: for m be Nat st n <=m holds ||. (h"(#)(f/*(h*z+c) - f
/*c)).m- dv.|| < r by A7,NORMSP_1:def 7;
x0 in N by NFCONT_1:4;
then
A25: rng c c= dom f by A1,A6,ZFMISC_1:31;
A26: n in NAT by ORDINAL1:def 12;
A27: P[n,h.n] by A11,A26;
||. (h"(#)(f/*(h*z+c) - f/*c)).n- dv.|| = ||.(h".n)*((f/*(h*z+c) - f
/*c).n)- dv.|| by NDIFF_1:def 2
.= ||.(h.n)"*((f/*(h*z+c) - f/*c).n)- dv.|| by VALUED_1:10
.= ||.(h.n)"*( (f/*(h*z+c)).n - (f/*c).n)- dv.|| by NORMSP_1:def 3
.= ||.(h.n)"*( (f/*(h*z+c)).n - f/.(c.n)) - dv.|| by A25,FUNCT_2:109,A26
.= ||.(h.n)"*( (f/*(h*z+c)).n - f/.x0) - dv.|| by FUNCOP_1:7,A26
.= ||.(h.n)"*( f/.( (h*z+c).n) - f/.x0) - dv.|| by A1,A23,FUNCT_2:109,A26
,XBOOLE_1:1
.= ||.(h.n)"*( f/.((h*z).n+c.n) - f/.x0) - dv.|| by NORMSP_1:def 2
.= ||.(h.n)"*( f/.((h*z).n+x0) - f/.x0) - dv.|| by FUNCOP_1:7,A26
.= ||.(h.n)"*(f/.((h.n)*z+x0) - f/.x0)-dv .|| by NDIFF_1:def 3;
hence
for e be Real
st e > 0 holds ex d be Real st d > 0 & for h be
Real st
|.h.| < d & h <> 0 & h*z+x0 in N holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv .|| <
e by A24,A27;
end;
now
assume
A28: for e be Real st e > 0 holds
ex d be Real st d > 0 & for h be Real st
|.h.| < d & h <> 0 & h*z+x0 in N holds ||. h"*(f/.(h*z+x0) - f/.x0) -
dv .|| < e;
now
let h be 0-convergent non-zero Real_Sequence;
let c such that
A29: rng c = {x0} and
A30: rng (h*z+c) c= N;
A31: h is convergent & lim h = 0;
x0 in N by NFCONT_1:4;
then
A32: rng c c= dom f by A1,A29,ZFMISC_1:31;
A33: for n be Element of NAT holds c.n=x0
proof
let n be Element of NAT;
c.n in rng c by NFCONT_1:6;
hence thesis by A29,TARSKI:def 1;
end;
A34: now
let r be Real;
assume r > 0;
then consider d be Real such that
A35: d > 0 and
A36: for h be Real st
|.h.| < d & h <> 0 & h*z+x0 in N holds ||.
h"*(f/.(h*z+x0) - f/.x0) - dv .|| < r by A28;
consider n be Nat such that
A37: for m be Nat st n <=m holds |.h.m-0 .| < d by A31,A35,
SEQ_2:def 7;
take n;
thus for m be Nat st n <=m holds ||. (h"(#)(f/*(h*z+c) - f
/*c)).m- dv.|| < r
proof
let m be Nat;
A38: m in NAT by ORDINAL1:def 12;
A39: h.m <> 0 by SEQ_1:5;
assume n <= m;
then
A40: |.h.m-0 .| < d by A37;
(h*z+c).m in rng (h*z+c) by NFCONT_1:6;
then (h*z+c).m in N by A30;
then (h*z).m+c.m in N by NORMSP_1:def 2;
then h.m*z + c.m in N by NDIFF_1:def 3;
then
A41: h.m*z + x0 in N by A33,A38;
||. (h"(#)(f/*(h*z+c) - f/*c)).m- dv.|| = ||.(h".m)*((f/*(h*z+c
) - f/*c).m)- dv.|| by NDIFF_1:def 2
.= ||.(h.m)"*((f/*(h*z+c) - f/*c).m)- dv.|| by VALUED_1:10
.= ||.(h.m)"*( (f/*(h*z+c)).m - (f/*c).m)- dv.|| by NORMSP_1:def 3
.= ||.(h.m)"*( (f/*(h*z+c)).m - f/.(c.m)) - dv.|| by A32,
FUNCT_2:109,A38
.= ||.(h.m)"*( (f/*(h*z+c)).m - f/.x0) - dv.|| by A33,A38
.= ||.(h.m)"*( f/.( (h*z+c).m) - f/.x0) - dv.|| by A1,A30,
FUNCT_2:109,XBOOLE_1:1,A38
.= ||.(h.m)"*( f/.((h*z).m+c.m) - f/.x0) - dv.|| by NORMSP_1:def 2
.= ||.(h.m)"*( f/.((h*z).m+x0) - f/.x0) - dv.|| by A33,A38
.= ||.(h.m)"*(f/.((h.m)*z+x0) - f/.x0)-dv .|| by NDIFF_1:def 3;
hence thesis by A36,A40,A39,A41;
end;
end;
hence (h"(#)(f/*(h*z+c) - f/*c)) is convergent by NORMSP_1:def 6;
hence lim (h"(#)(f/*(h*z+c) - f/*c)) = dv by A34,NORMSP_1:def 7;
end;
hence
for h be 0-convergent non-zero Real_Sequence for c 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));
end;
hence thesis by A2;
end;
definition
let S,T;
let f;
let x0 be Point of S;
let z be Point of S;
pred f is_Gateaux_differentiable_in x0,z means
ex N be Neighbourhood
of x0 st N c= dom f & ex dv be Point of T st
for e be Real st e > 0 holds ex d be Real st d > 0 &
for h be Real st |.h.| < d & h <> 0 & h*z+x0 in N holds ||.
h"*(f/.(h*z+x0) - f/.x0) - dv .|| < e;
end;
theorem Th4:
(for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| > 0
iff x <> y) &
(for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| = ||.y
-x.||) &
(for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| = 0 iff x =
y) & (for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| <> 0 iff x <> y
) & (for X be RealNormSpace, x,y,z be Point of X,
e be Real st e > 0 holds ( (
||.x-z.||