:: Differentiable Functions on Normed Linear Spaces. {P}art {II}
:: by Hiroshi Imura , Yuji Sakai and Yasunari Shidama
::
:: Received June 4, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, NAT_1,
FDIFF_1, SUBSET_1, LOPBAN_1, RELAT_1, RSSPACE, RCOMP_1, TARSKI, SEQ_1,
ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2, ORDINAL2, SUPINF_2, FCONT_1,
COMPLEX1, STRUCT_0, CARD_1, VALUED_0, XXREAL_0, FUNCOP_1, XBOOLE_0,
NDIFF_2;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1,
FUNCOP_1, RLVECT_1, PRE_TOPC, STRUCT_0, VALUED_0, VALUED_1, SEQ_1, SEQ_2,
VFUNCT_1, NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, NFCONT_1, FDIFF_1,
NDIFF_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1,
NFCONT_1, NDIFF_1, VALUED_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, MEMBERED, FDIFF_1,
STRUCT_0, LOPBAN_1, NDIFF_1, VALUED_1, FUNCT_2, NUMBERS, VALUED_0,
FUNCOP_1, NAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RLVECT_1;
expansions TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1,
ZFMISC_1, SEQ_1, SEQ_2, NAT_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2,
SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_2, LOPBAN_3, PARTFUN1, PARTFUN2,
NFCONT_1, FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0,
VALUED_1, VALUED_0, ORDINAL1, VECTSP_1, NORMSP_0, XREAL_0;
schemes FUNCT_2;
begin :: Differentiable Functions on Normed Linear Spaces
reserve p for Real;
reserve S,T for RealNormSpace;
reserve x0 for Point of S;
reserve f for PartFunc of S,T;
reserve c for constant sequence of S;
reserve R for RestFunc of S,T;
definition
let X,Y,Z be RealNormSpace;
let f be Element of BoundedLinearOperators(X,Y);
let g be Element of BoundedLinearOperators(Y,Z);
func g*f -> Element of BoundedLinearOperators(X,Z) equals
modetrans(g,Y,Z)*
modetrans(f,X,Y);
correctness
proof
modetrans(g,Y,Z)*modetrans(f,X,Y) is Lipschitzian LinearOperator of X,Z by
LOPBAN_2:2;
hence thesis by LOPBAN_1:def 9;
end;
end;
definition
let X,Y,Z be RealNormSpace;
let f be Point of R_NormSpace_of_BoundedLinearOperators(X,Y);
let g be Point of R_NormSpace_of_BoundedLinearOperators(Y,Z);
func g*f -> Point of R_NormSpace_of_BoundedLinearOperators(X,Z) equals
modetrans(g,Y,Z)*modetrans(f,X,Y);
correctness
proof
R_NormSpace_of_BoundedLinearOperators(X,Z) = NORMSTR (#
BoundedLinearOperators(X,Z), Zero_(BoundedLinearOperators(X,Z),
R_VectorSpace_of_LinearOperators(X,Z)), Add_(BoundedLinearOperators(X,Z),
R_VectorSpace_of_LinearOperators(X,Z)), Mult_(BoundedLinearOperators(X,Z),
R_VectorSpace_of_LinearOperators(X,Z)), BoundedLinearOperatorsNorm(X,Z) #) &
modetrans(g,Y,Z)*modetrans(f,X,Y) is Lipschitzian LinearOperator of X,Z by
LOPBAN_1:def 14,LOPBAN_2:2;
hence thesis by LOPBAN_1:def 9;
end;
end;
theorem Th1:
for x0 be Point of S st f is_differentiable_in x0 ex N being
Neighbourhood of x0 st ( N c= dom f & for z be Point of S holds 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 & diff(f,x0).z = lim (h"(#)(f/*(h*z+c) - f
/*c)) )
proof
let x0 be Point of S;
assume f is_differentiable_in x0;
then consider N be Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st
x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0) by NDIFF_1:47;
consider R such that
A3: R/.0.S=0.T and
R is_continuous_in 0.S and
A4: for x be Point of S st x in N holds f/.x - f/.x0 = diff(f,x0).(x-x0)
+ R/.(x-x0) by A2;
now
let z be Point of S;
let h be 0-convergent non-zero Real_Sequence;
let c such that
A5: rng c = {x0} and
A6: rng (h*z+c) c= N;
A7: abs(h)"(#)(R/*(h*z)) is convergent & lim ( abs(h)"(#)(R/*(h*z)) ) = 0.T
proof
now
per cases;
case
A8: z= 0.S;
for n be Nat holds (abs(h)"(#) (R/*(h*z))).n = 0.T
proof
let n be Nat;
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A9: rng (h*z) c= dom R;
A10: n in NAT by ORDINAL1:def 12;
thus (abs(h)"(#)(R/*(h*z))).n =abs(h)".n*(R/*(h*z)).n by
NDIFF_1:def 2
.=(abs(h).n)"*(R/*(h*z)).n by VALUED_1:10
.=(|.h.n.|)"*(R/*(h*z)).n by SEQ_1:12
.= (|.h.n.|)"*(R/.((h*z).n)) by A10,A9,FUNCT_2:109
.= (|.h.n.|)"*(R/.(h.n*0.S)) by A8,NDIFF_1:def 3
.= (|.h.n.|)"*(R/.(0.S)) by RLVECT_1:10
.=0.T by A3,RLVECT_1:10;
end;
then
abs(h)"(#) (R/*(h*z)) is constant & (abs(h)"(#) (R/*(h*z))).0 =
0.T by VALUED_0:def 18;
hence thesis by NDIFF_1:18;
end;
case
z<> 0.S;
then
A11: (h*z) is non-zero (0.S)-convergent by NDIFF_1:21;
then reconsider s = h*z as (0.S)-convergent sequence of S ;
now
let n be Element of NAT;
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A12: rng s c= dom R;
h.n <> 0 by SEQ_1:5;
then
A13: |.h.n.| <> 0 by COMPLEX1:47;
s.n <> 0.S by NDIFF_1:7,A11;
then
A14: ||.s.n.|| <> 0 by NORMSP_0:def 5;
||.s.n.|| = ||.(h.n)*z.|| by NDIFF_1:def 3
.= |.h.n.| * ||.z.|| by NORMSP_1:def 1;
then (|.h.n.|)"* ||.s.n.|| = ((|.h.n.|)"* (|.h.n.|)) * ||.z.||
.= 1 * ||.z.|| by A13,XCMPLX_0:def 7
.= ||.z.||;
then ||.z.|| *( ||.s.n.|| )" = (|.h.n.|)"* (||.s.n.|| *( ||.s.n
.|| )")
.= (|.h.n.|)"* (||.s.n.|| /( ||.s.n.|| )) by XCMPLX_0:def 9
.= (|.h.n.|)"*1 by A14,XCMPLX_1:60
.= (|.h.n.|)";
then
A15: ||.z.|| *( ||.s.||.n )" = (|.h.n.|)" by NORMSP_0:def 4;
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A16: rng (h*z) c= dom R;
thus (abs(h)"(#)(R/*(h*z))).n = abs(h)".n*(R/*(h*z)).n by
NDIFF_1:def 2
.=(abs(h).n)"*(R/*(h*z)).n by VALUED_1:10
.=(|.h.n.|)"*(R/*(h*z)).n by SEQ_1:12
.= (|.h.n.|)"*(R/.((h*z).n)) by A16,FUNCT_2:109
.= ( ||.z.|| *||.s.||".n)*(R/.(s.n)) by A15,VALUED_1:10
.= ||.z.|| *(||.s.||".n *(R/.(s.n)) ) by RLVECT_1:def 7
.= ||.z.|| *((||.s.||".n)*((R/*s).n)) by A12,FUNCT_2:109
.= ||.z.|| *((||.s.||")(#)(R/*s)).n by NDIFF_1:def 2
.= ( ||.z.|| *((||.s.||")(#)(R/*s))).n by NORMSP_1:def 5;
end;
then
A17: (abs(h)"(#)(R/*(h*z))) = ||.z.|| *((||.s.||")(#)(R/*s)) by FUNCT_2:63
;
A18: (||.s.||")(#)(R/*s) is convergent by A11,NDIFF_1:def 5;
hence (abs(h)"(#)(R/*(h*z))) is convergent by A17,NORMSP_1:22;
lim ((||.s.||")(#)(R/*s)) = 0.T by A11,NDIFF_1:def 5;
hence lim (abs(h)"(#)(R/*(h*z))) = ||.z.|| * 0.T by A17,A18,
NORMSP_1:28
.= 0.T by RLVECT_1:10;
end;
end;
hence thesis;
end;
A19: now
let e be Real;
assume 0 < e;
then consider m be Nat such that
A20: for n be Nat st m <= n holds ||.(abs(h)"(#) (R/*(h*z
))).n - 0.T .|| < e by A7,NORMSP_1:def 7;
now
let n be Nat such that
A21: m <= n;
||.(h"(#) (R/*(h*z))).n -0.T .|| = ||.(h"(#) (R/*(h*z))).n .|| by
RLVECT_1:13
.= ||.h".n*(R/*(h*z)).n .|| by NDIFF_1:def 2
.= ||.(h.n)"*(R/*(h*z)).n .|| by VALUED_1:10
.= |.|.(h.n)".|.| * ||.(R/*(h*z)).n .|| by NORMSP_1:def 1
.= ||.|.(h.n)".|*(R/*(h*z)).n .|| by NORMSP_1:def 1
.= ||.|.h".n.|*(R/*(h*z)).n .|| by VALUED_1:10
.= ||.abs(h").n*(R/*(h*z)).n .|| by SEQ_1:12
.= ||.(abs(h))".n*(R/*(h*z)).n .|| by SEQ_1:54
.= ||.(abs(h)"(#) (R/*(h*z))).n .|| by NDIFF_1:def 2
.= ||.(abs(h)"(#) (R/*(h*z))).n -0.T .|| by RLVECT_1:13;
hence ||.(h"(#) (R/*(h*z))).n -0.T .|| < e by A20,A21;
end;
hence ex m be Nat st for n be Nat st m <= n holds
||.(h"(#) (R/*(h*z))).n -0.T .|| < e;
end;
x0 in N by NFCONT_1:4;
then
A22: rng c c= dom f by A1,A5,ZFMISC_1:31;
A23: for n be Nat holds ||. (h"(#)(f/*(h*z+c) - f/*c)).n - diff
(f,x0).z .|| = ||. (h"(#) (R/*(h*z))).n .||
proof
R is total by NDIFF_1:def 5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A24: rng (h*z) c= dom R;
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider
L = diff(f,x0) as Element of BoundedLinearOperators(S,T);
let n be Nat;
A25: n in NAT by ORDINAL1:def 12;
A26: h.n <> 0 by SEQ_1:5;
dom c = NAT by FUNCT_2:def 1;
then c.n in rng c by FUNCT_1:3,A25;
then
A27: c.n=x0 by A5,TARSKI:def 1;
dom (h*z+c) = NAT by FUNCT_2:def 1;
then (h*z+c).n in rng (h*z+c) by FUNCT_1:3,A25;
then (h*z+c).n in N by A6;
then (h*z).n+c.n in N by NORMSP_1:def 2;
then
A28: h.n*z+x0 in N by A27,NDIFF_1:def 3;
(h"(#)(f/*(h*z+c) - f/*c)).n - diff(f,x0).z = (h".n) * (f/*(h*z+c)
- f/*c).n - diff(f,x0).z by NDIFF_1:def 2
.= (h.n)" * (f/*(h*z+c) - f/*c).n - diff(f,x0).z by VALUED_1:10
.= (h.n)" * ((f/*(h*z+c)).n - (f/*c).n) - diff(f,x0).z by
NORMSP_1:def 3
.= (h.n)" * (f/.((h*z+c).n) - (f/*c).n) - diff(f,x0).z by A1,A6,
FUNCT_2:109,XBOOLE_1:1,A25
.= (h.n)" * (f/.((h*z+c).n) - f/.(c.n) )- diff(f,x0).z by A22,
FUNCT_2:109,A25
.= (h.n)" * (f/.((h*z).n+c.n) - f/.(c.n) )- diff(f,x0).z by
NORMSP_1:def 2
.= (h.n)" * (f/.(h.n*z+c.n) - f/.(c.n) )- diff(f,x0).z by NDIFF_1:def 3
.= (h.n)" * (diff(f,x0).(h.n*z+x0-x0) + R/.(h.n*z+x0-x0)) - diff(f,
x0).z by A4,A27,A28
.= (h.n)" * (diff(f,x0).(h.n*z+(x0-x0)) + R/.(h.n*z+x0-x0)) - diff(f
,x0).z by RLVECT_1:def 3
.= (h.n)" * (diff(f,x0).(h.n*z+(x0-x0)) + R/.(h.n*z+(x0-x0))) - diff
(f,x0).z by RLVECT_1:def 3
.= (h.n)" * (diff(f,x0).(h.n*z+0.S) + R/.(h.n*z+(x0-x0))) - diff(f,
x0).z by RLVECT_1:15
.= (h.n)" * (diff(f,x0).(h.n*z+0.S) + R/.(h.n*z+0.S)) - diff(f,x0).z
by RLVECT_1:15
.= (h.n)" * (diff(f,x0).(h.n*z) + R/.(h.n*z+0.S)) - diff(f,x0).z by
RLVECT_1:4
.= (h.n)" * (diff(f,x0).(h.n*z) + R/.(h.n*z)) - diff(f,x0).z by
RLVECT_1:4
.= (h.n)" * (R/.(h.n*z))+(h.n)" * (diff(f,x0).(h.n*z)) - diff(f,x0).
z by RLVECT_1:def 5
.= (h.n)" * (R/.(h.n*z))+(h.n)" * (modetrans(L,S,T).(h.n*z)) - diff(
f,x0).z by LOPBAN_1:def 11
.= (h.n)" * (R/.(h.n*z))+(h.n)" * (h.n* (modetrans(L,S,T).z)) - diff
(f,x0).z by LOPBAN_1:def 5
.= (h.n)" * (R/.(h.n*z))+(h.n)" * (h.n* (L.z)) - diff(f,x0).z by
LOPBAN_1:def 11
.= (h.n)" * (R/.(h.n*z))+(h.n)" * (h.n)* (diff(f,x0).z) - diff(f,x0)
.z by RLVECT_1:def 7
.= (h.n)" * (R/.(h.n*z))+1* (diff(f,x0).z) - diff(f,x0).z by A26,
XCMPLX_0:def 7
.= (h.n)" * (R/.(h.n*z))+(diff(f,x0).z) - diff(f,x0).z by
RLVECT_1:def 8
.= (h.n)" * (R/.(h.n*z))+(diff(f,x0).z - diff(f,x0).z) by
RLVECT_1:def 3
.= (h.n)" * (R/.(h.n*z))+0.T by RLVECT_1:15
.= (h.n)" * (R/.(h.n*z)) by RLVECT_1:4
.= (h".n) * (R/.(h.n*z)) by VALUED_1:10
.= (h".n) * (R/.((h*z).n)) by NDIFF_1:def 3
.= (h".n) * ((R/*(h*z)).n) by A24,FUNCT_2:109,A25
.=(h"(#) (R/*(h*z))).n by NDIFF_1:def 2;
hence thesis;
end;
A29: now
let e be Real;
assume 0 < e;
then consider m be Nat such that
A30: for n be Nat st m <= n holds ||.(h"(#) (R/*(h*z))).n
- 0.T .|| < e by A19;
now
let n be Nat;
assume m <= n;
then ||.(h"(#) (R/*(h*z))).n -0.T .|| < e by A30;
then ||.(h"(#) (R/*(h*z))).n .|| < e by RLVECT_1:13;
hence ||. (h"(#)(f/*(h*z+c) - f/*c)).n - diff(f,x0).z .|| < e by A23;
end;
hence ex m be Nat st for n be Nat st m <= n holds
||. (h"(#)(f/*(h*z+c) - f/*c)).n - diff(f,x0).z .|| < e;
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)) = diff(f,x0).z by A29,NORMSP_1:def 7;
end;
hence thesis by A1;
end;
theorem
for x0 be Point of S st f is_differentiable_in x0 for z be Point of S
for h be 0-convergent non-zero Real_Sequence
for c st rng c = {x0} & rng (h*z+c) c=
dom f holds h"(#)(f/*(h*z+c) - f/*c) is convergent & diff(f,x0).z = lim (h"(#)(
f/*(h*z+c) - f/*c))
proof
let x0 be Point of S;
assume f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: for z be Point of S holds 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 & diff(f,x0).z = lim (h"(#)(f/*(h*z+c) - f/*c)) by Th1;
let z be Point of S;
let h be 0-convergent non-zero Real_Sequence;
let c such that
A3: rng c = {x0} and
A4: rng (h*z+c) c= dom f;
x0 in N by NFCONT_1:4;
then
A5: rng c c= dom f by A3,A1,ZFMISC_1:31;
consider g be Real such that
A6: 0<g and
A7: {y where y is Point of S: ||.y-x0.|| < g} c= N by NFCONT_1:def 1;
A8: 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 A3,TARSKI:def 1;
end;
ex n being Element of NAT st rng ((h^\n*z+c)) c= N
proof
A9: now
let p;
assume
A10: 0<p;
ex pp be Real st pp > 0 & pp*||.z.|| < p
proof
take pp=p/(||.z.||+1);
A11: ||.z.||+0 < ||.z.||+1 & 0 <= ||.z.|| by NORMSP_1:4,XREAL_1:8;
A12: ||.z.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/( ||.z.||+1 ) by A10,XREAL_1:139;
then pp* ||.z.|| < pp*( ||.z.|| + 1) by A11,XREAL_1:97;
hence thesis by A10,A12,XCMPLX_1:87;
end;
then consider pp be Real such that
A13: pp > 0 and
A14: pp*||.z.|| < p;
h is convergent & lim h =0;
then consider n be Nat such that
A15: for m be Nat st n <= m holds |.h.m- 0 .| < pp by A13,
SEQ_2:def 7;
take n;
let m be Nat;
assume n<=m;
then
A16: |.h.m-0 .| < pp by A15;
A17: ||.(h*z).m-0.S.|| = ||.h.m*z - 0.S.|| by NDIFF_1:def 3
.= ||.h.m*z.|| by RLVECT_1:13
.= |.h.m.|*||.z.|| by NORMSP_1:def 1;
0 <= ||.z.|| by NORMSP_1:4;
then |.h.m.|*||.z.|| <= pp* ||.z.|| by A16,XREAL_1:64;
hence ||.(h*z).m-0.S.||<p by A14,A17,XXREAL_0:2;
end;
then
A18: h*z is convergent by NORMSP_1:def 6;
c.0 in rng c by NFCONT_1:6;
then c.0=x0 by A3,TARSKI:def 1;
then
A19: lim c = x0 by NDIFF_1:18;
A20: c is convergent by NDIFF_1:18;
then
A21: h*z + c is convergent by A18,NORMSP_1:19;
lim (h*z) = 0.S by A9,A18,NORMSP_1:def 7;
then lim ((h*z) + c) = 0.S + x0 by A20,A19,A18,NORMSP_1:25
.= x0 by RLVECT_1:4;
then consider n being Nat such that
A22: for m being Nat st n<=m holds ||.(h*z+c).m-x0.||<g by A6,A21,
NORMSP_1:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
let y be object;
assume y in rng ((h^\n*z+c));
then consider m be Nat such that
A23: y = ((h^\n*z+c)).m by NFCONT_1:6;
A24: n+m in NAT by ORDINAL1:def 12;
A25: m in NAT by ORDINAL1:def 12;
reconsider y1=y as Point of S by A23;
||.(h*z+c).(n+m)-x0.||<g by A22,NAT_1:11;
then ||.((h*z).(n+m)+c.(n+m)) -x0.||<g by NORMSP_1:def 2;
then ||.((h*z).(n+m)+x0) -x0.||<g by A8,A24;
then ||.((h*z).(n+m)+c.m) -x0.||<g by A8,A25;
then ||.((h.(n+m)*z)+c.m) -x0.||<g by NDIFF_1:def 3;
then ||.((h^\n).m*z+c.m) -x0.||<g by NAT_1:def 3;
then ||.(((h^\n)*z).m+c.m) -x0.||<g by NDIFF_1:def 3;
then ||.((h^\n*z+c)).m - x0 .|| < g by NORMSP_1:def 2;
then y1 in {w where w is Point of S: ||.w-x0.|| < g} by A23;
hence thesis by A7;
end;
then consider n be Element of NAT such that
A26: rng ((h^\n*z+c)) c= N;
A27: now
let m be Element of NAT;
thus ((h*z+c)^\n).m = (h*z+c).(n+m) by NAT_1:def 3
.= (h*z).(n+m)+c.(n+m) by NORMSP_1:def 2
.=(h*z).(n+m)+x0 by A8
.=(h*z).(n+m)+c.m by A8
.=(h.(n+m)*z)+c.m by NDIFF_1:def 3
.=(h^\n).m*z+c.m by NAT_1:def 3
.=((h^\n)*z).m+c.m by NDIFF_1:def 3
.=(h^\n*z+c).m by NORMSP_1:def 2;
end;
now
let m be Element of NAT;
A28: ((f/*(h*z+c))^\n).m =(f/*(h*z+c)).(n+m) by NAT_1:def 3
.=f/.((h*z+c).(n+m)) by A4,FUNCT_2:109
.=f/.( ( (h*z+c)^\n).m) by NAT_1:def 3
.=f/.( (h^\n*z+c).m) by A27;
thus ( (h"(#)(f/*(h*z+c) - f/*c))^\n).m =(h"(#)(f/*(h*z+c) - f/*c)).(n+m)
by NAT_1:def 3
.=h".(n+m)*(f/*(h*z+c) - f/*c).(n+m) by NDIFF_1:def 2
.=(h.(n+m))"*(f/*(h*z+c) - f/*c).(n+m) by VALUED_1:10
.=((h^\n).m)"*(f/*(h*z+c) - f/*c).(n+m) by NAT_1:def 3
.=((h^\n).m)"*((f/*(h*z+c)).(n+m) - (f/*c).(n+m)) by NORMSP_1:def 3
.=((h^\n).m)"*(((f/*(h*z+c))^\n).m - (f/*c).(n+m)) by NAT_1:def 3
.=((h^\n).m)"*(f/.( (h^\n*z+c).m) - f/.(c.(n+m))) by A5,A28,FUNCT_2:109
.=((h^\n).m)"*(f/.( (h^\n*z+c).m) - f/.x0) by A8
.=((h^\n).m)"*(f/.( (h^\n*z+c).m) - f/.(c.m)) by A8
.=((h^\n).m)"*(f/.((h^\n*z+c).m) - (f/*c).m) by A5,FUNCT_2:109
.=((h^\n).m)"*((f/*(h^\n*z+c)).m - (f/*c).m) by A1,A26,FUNCT_2:109
,XBOOLE_1:1
.=((h^\n).m)"*((f/*(h^\n*z+c) - f/*c).m) by NORMSP_1:def 3
.=((h^\n)".m)*(f/*(h^\n*z+c) - f/*c).m by VALUED_1:10
.=((h^\n)"(#)(f/*(h^\n*z+c) - f/*c)).m by NDIFF_1:def 2;
end;
then
A29: (h^\n)"(#)(f/*(h^\n*z+c) - f/*c) = (h"(#)(f/*(h*z+c) - f/*c))^\n by
FUNCT_2:63;
(h^\n)"(#)(f/*(h^\n*z+c) - f/*c) is convergent & diff(f,x0).z = lim ((h
^\n)" (#)(f/*(h^\n*z+c) - f/*c)) by A3,A2,A26;
hence thesis by A29,LOPBAN_3:10,11;
end;
theorem Th3:
for x0 be Point of S for N be Neighbourhood of x0 st N c= dom f
for z be Point of S for dv be Point of T holds
( (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))) iff 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 )
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;
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<p;
consider n being Nat such that
A14: p"<n by SEQ_4:3;
p" + 0 < n + 1 by A14,XREAL_1:8;
then 1/(n+1) < 1/p" by A13,XREAL_1:76;
then
A15: 1/(n+1) < p by XCMPLX_1:216;
take n;
let m be Nat;
assume n<=m;
then
A16: n + 1 <= m + 1 by XREAL_1:6;
m in NAT by ORDINAL1:def 12;
then
A17: P[m,h.m] by A11;
1/(m+1) <= 1/(n+1) by A16,XREAL_1:118;
then |.h.m-0 .| < 1/(n+1) by A17,XXREAL_0:2;
hence |.h.m-0 .| <p by A15,XXREAL_0:2;
end;
then
A18: h is convergent by SEQ_2:def 6;
then
A19: lim h = 0 by A12,SEQ_2:def 7;
for n be Nat holds h.n <> 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.|| <e/2 & ||.z-y.|| <e/2) implies ||.x-y.|| <e) ) & (for X be
RealNormSpace, x,y,z be Point of X, e be Real st
e > 0 holds ((||.x-z.|| <e/2
& ||.y-z.|| <e/2) implies ||.x-y.|| <e) ) & (for X be RealNormSpace, x be Point
of X st ( for e be Real st e>0
holds ||.x.|| <e ) holds x=0.X ) & for X be
RealNormSpace, x,y be Point of X st ( for e be Real
st e>0 holds ||.x-y.|| <e )
holds x=y
proof
thus for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| > 0 iff x <> y
proof
let X be RealNormSpace;
let x, y be Point of X;
0 < ||.x-y.|| implies x-y <> 0.X by NORMSP_0:def 6;
hence 0 < ||.x-y.|| implies x <> y by RLVECT_1:15;
now
assume x <> y;
then 0 <> ||.x-y.|| by NORMSP_1:11;
hence 0 < ||.x-y.|| by NORMSP_1:4;
end;
hence thesis;
end;
thus for X be RealNormSpace, x,y be Point of X holds ||.x-y.|| = ||.y-x.||
proof
let X be RealNormSpace;
let x, y be Point of X;
thus ||.x-y.|| = ||.-(x-y).|| by NORMSP_1:2
.= ||.y-x.|| by RLVECT_1:33;
end;
A1: for X be RealNormSpace for x, y, z be Point of X
for e be Real st e > 0
holds ( ||.x-z.|| < e/2 & ||.z-y.|| < e/2 implies ||.x-y.|| <e)
proof
let X be RealNormSpace;
let x, y, z be Point of X;
let e be Real such that
e > 0;
assume ||.x-z.|| < e/2 & ||.z-y.|| < e/2;
then ||.x-z.|| + ||.z-y.|| < e/2 + e/2 by XREAL_1:8;
then ||.x-y.|| + (||.x-z.|| + ||.z-y.||) < (||.x-z.|| + ||.z-y.||) + e by
NORMSP_1:10,XREAL_1:8;
then
||.x-y.|| + (||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) < e + (
||.x-z.|| + ||.z-y.||) +- (||.x-z.|| + ||.z-y.||) by XREAL_1:8;
hence thesis;
end;
A2: for X be RealNormSpace for x, y, z be Point of X
for e be Real st e > 0
holds ( ||.x-z.|| < e/2 & ||.y-z.|| < e/2 implies ||.x-y.|| < e)
proof
let X be RealNormSpace;
let x, y, z be Point of X;
let e be Real such that
A3: e > 0;
assume that
A4: ||.x-z.|| < e/2 and
A5: ||.y-z.|| < e/2;
||.-(y-z).|| < e/2 by A5,NORMSP_1:2;
then ||.z-y.|| < e/2 by RLVECT_1:33;
hence thesis by A1,A3,A4;
end;
A6: for X be RealNormSpace for x be Point of X st
(for e be Real st e>0
holds ||.x.|| <e) holds x=0.X
proof
let X be RealNormSpace;
let x be Point of X such that
A7: for e be Real st e > 0 holds ||.x.|| <e;
now
assume x<>0.X;
then 0 <> ||.x.|| by NORMSP_0:def 5;
then 0 < ||.x.|| by NORMSP_1:4;
hence contradiction by A7;
end;
hence thesis;
end;
for X be RealNormSpace for x,y be Point of X st
(for e be Real st e>0 holds ||.x-y.|| <e) holds x=y
proof
let X be RealNormSpace;
let x,y be Point of X;
assume for e be Real st e > 0 holds ||.x-y.|| <e;
then x-y = 0.X by A6;
hence thesis by RLVECT_1:21;
end;
hence thesis by A1,A2,A6,NORMSP_1:6;
end;
definition
let S,T;
let f;
let x0 be Point of S;
let z be Point of S;
assume
A1: f is_Gateaux_differentiable_in x0,z;
func Gateaux_diff(f,x0,z) -> Point of T means
:Def4:
ex N be Neighbourhood
of x0 st N c= dom f &
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) - it .|| < e;
existence
by A1;
uniqueness
proof
let dv1,dv2 be Point of T;
assume that
A2: ex N1 be Neighbourhood of x0 st N1 c= dom f &
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 N1 holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv1 .|| < e and
A3: ex N2 be Neighbourhood of x0 st N2 c= dom f &
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 N2 holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv2 .|| < e;
consider N2 be Neighbourhood of x0 such that
N2 c= dom f and
A4: 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 N2 holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv2
.|| < e by A3;
consider N1 be Neighbourhood of x0 such that
N1 c= dom f and
A5: 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 N1 holds ||. h"*(f/.(h*z+x0) - f/.x0) - dv1
.|| < e by A2;
now
let e be Real such that
A6: e > 0;
A7: 0 < e/2 by A6,XREAL_1:215;
then consider d1 be Real such that
A8: d1 > 0 and
A9: for h be Real st
|.h.| < d1 & h <> 0 & h*z+x0 in N1 holds ||.
h"*(f/.(h*z+x0) - f/.x0) - dv1 .|| < e/2 by A5;
consider d2 be Real such that
A10: d2 > 0 and
A11: for h be Real st |.h.| < d2 & h <> 0 & h*z+x0 in N2 holds ||.
h"*(f/.(h*z+x0) - f/.x0) - dv2 .|| < e/2 by A4,A7;
ex h be Real st h <> 0 &
|.h.| < d1 & |.h.| < d2 & h*z+x0 in N1 &
h*z+x0 in N2
proof
set d3=min(d1,d2);
consider N0 be Neighbourhood of x0 such that
A12: N0 c= N1 & N0 c= N2 by NDIFF_1:1;
consider g be Real such that
A13: 0<g and
A14: {y where y is Point of S: ||.y - x0.|| < g} c= N0 by NFCONT_1:def 1;
consider n0 be Nat such that
A15: ||.z.|| /g < n0 by SEQ_4:3;
set n1=n0+1;
set h = min(1/(n1+1), d3/2);
take h;
A16: h <=d3/2 by XXREAL_0:17;
A17: 0 < d3 by A8,A10,XXREAL_0:15;
then
A18: 0 < d3/2 by XREAL_1:215;
0 < 1 * (1 + n1)";
then
A19: 0 < 1/(1 + n1) by XCMPLX_0:def 9;
hence h <> 0 by A18,XXREAL_0:15;
A20: 0 < h by A18,A19,XXREAL_0:15;
n0 <= n0+1 by NAT_1:11;
then ||.z.|| /g < (n0+1) by A15,XXREAL_0:2;
then ( ||.z.|| /g)*g < (n0+1)*g by A13,XREAL_1:68;
then ||.z.|| < (n0+1)*g by A13,XCMPLX_1:87;
then
A21: ||.z.|| /(n0+1) < g by XREAL_1:83;
A22: ||.h*z+x0-x0.|| = ||.h*z+(x0-x0).|| by RLVECT_1:def 3
.= ||.h*z+0.S.|| by RLVECT_1:15
.= ||.h*z.|| by RLVECT_1:4
.= |.h.|*||.z.|| by NORMSP_1:def 1
.= h* ||.z.|| by A20,ABSVALUE:def 1;
A23: d3/2 < d3 by A17,XREAL_1:216;
d3 <=d2 by XXREAL_0:17;
then d3/2 < d2 by A23,XXREAL_0:2;
then
A24: h < d2 by A16,XXREAL_0:2;
d3<=d1 by XXREAL_0:17;
then d3/2 < d1 by A23,XXREAL_0:2;
then h < d1 by A16,XXREAL_0:2;
hence |.h.| < d1 & |.h.| < d2 by A20,A24,ABSVALUE:def 1;
0 <= ||.z.|| by NORMSP_1:4;
then
A25: h* ||.z.|| <=(1/(n1+1)) * ||.z.|| by XREAL_1:64,XXREAL_0:17;
0 <= ||.z.|| & n1 <= 1+n1 by NAT_1:12,NORMSP_1:4;
then
A26: ||.z.|| /(1+n1) <= ||.z.|| /n1 by XREAL_1:118;
( 1 /(1+n1) )* ||.z.|| = ||.z.|| /(1+n1) by XCMPLX_1:99;
then ( 1 /(1+n1) )* ||.z.|| < g by A21,A26,XXREAL_0:2;
then ||.h*z+x0-x0.|| < g by A22,A25,XXREAL_0:2;
then (h*z+x0) in {y where y is Point of S: ||.y - x0.|| < g};
then (h*z+x0) in N0 by A14;
hence thesis by A12;
end;
then consider h be Real such that
A27: |.h.| < d1 and
A28: |.h.| < d2 and
A29: h <> 0 and
A30: h*z+x0 in N1 and
A31: h*z+x0 in N2;
||. h"*(f/.(h*z+x0) - f/.x0) - dv1 .|| < e/2 by A9,A27,A29,A30;
then
A32: ||. dv1- h"*(f/.(h*z+x0) - f/.x0) .|| < e/2 by Th4;
||. h"*(f/.(h*z+x0) - f/.x0) - dv2 .|| < e/2 by A11,A28,A29,A31;
hence ||. dv1- dv2 .|| < e by A6,A32,Th4;
end;
hence thesis by Th4;
end;
end;
theorem
for x0 be Point of S, z be 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 be Point of T st
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)) ) )
proof
let x0 be Point of S;
let z be Point of S;
A1: now
assume ex N being Neighbourhood of x0 st ( N c= dom f & ex dv be Point of
T st for h be 0-convergent non-zero Real_Sequence,
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)) );
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
A3: ex dv be Point of T st for h be 0-convergent non-zero Real_Sequence, 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));
consider dv be Point of T such that
A4: for h be 0-convergent non-zero Real_Sequence, 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)) by A3;
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 A2,A4,Th3;
hence f is_Gateaux_differentiable_in x0,z by A2;
end;
now
assume f is_Gateaux_differentiable_in x0,z;
then consider N being Neighbourhood of x0 such that
A5: N c= dom f and
A6: 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) -
Gateaux_diff(f,x0,z) .|| < e by Def4;
for h be 0-convergent non-zero Real_Sequence,
c 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 be Point of T
st for h be 0-convergent non-zero Real_Sequence,
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
)) ) by A5;
end;
hence thesis by A1;
end;
theorem
for x0 be Point of S st f is_differentiable_in x0 for z be 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 be 0-convergent non-zero
Real_Sequence, c 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))) )
proof
let x0 be Point of S;
assume f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: for z be Point of S holds for h be 0-convergent non-zero Real_Sequence, c
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 Th1;
let z be Point of S;
A3: for h be 0-convergent non-zero Real_Sequence,
c 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 A2;
then
A4: 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) - diff(f,
x0).z .|| < e by A1,Th3;
hence f is_Gateaux_differentiable_in x0,z by A1;
hence Gateaux_diff(f,x0,z)=diff(f,x0).z by A1,A4,Def4;
hence thesis by A1,A3;
end;
reserve U for RealNormSpace;
theorem Th7:
for R be RestFunc of S,T st R/.0.S=0.T
for e be Real st e > 0
ex d be Real st
d > 0 & for h be Point of S st ||.h.|| < d holds ||.R/.h.|| <= e*||.h
.||
proof
let R be RestFunc of S,T such that
A1: R/.0.S=0.T;
let e be Real such that
A2: e > 0;
R is total by NDIFF_1:def 5;
then consider d be Real such that
A3: d > 0 and
A4: for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||.
R/.z .||) < e by A2,NDIFF_1:23;
take d;
now
let h be Point of S such that
A5: ||.h.|| < d;
now
per cases;
case
A6: h <> 0.S;
then 0 <= ||.h.|| & ||.h.||"*||. R/.h .|| <= e by A4,A5,NORMSP_1:4;
then ||.h.||*(||.h.||"*||. R/.h .||) <= ||.h.||*e by XREAL_1:64;
then
A7: ||.h.||*||.h.||"*||. R/.h .|| <= e* ||.h.||;
||.h.|| <> 0 by A6,NORMSP_0:def 5;
then 1*||. R/.h .|| <= e* ||.h.|| by A7,XCMPLX_0:def 7;
hence ||. R/.h .|| <= e* ||.h.||;
end;
case
A8: h = 0.S;
0 <= ||.h.|| by NORMSP_1:4;
then 0* ||.h.|| <= e* ||.h.|| by A2;
hence ||. R/.h .|| <= e* ||.h.|| by A1,A8,NORMSP_0:def 6;
end;
end;
hence ||. R/.h .|| <= e* ||.h.||;
end;
hence thesis by A3;
end;
theorem
for R be RestFunc of T,U st R/.0.T=0.U
for L be Lipschitzian LinearOperator of
S,T holds R*L is RestFunc of S,U
proof
let R be RestFunc of T,U such that
A1: R/.0.T=0.U;
let L be Lipschitzian LinearOperator of S,T;
consider K be Real such that
A2: 0 <= K and
A3: for h be Point of S holds ||.L.h.|| <= K * ||.h.|| by LOPBAN_1:def 8;
A4: dom L = the carrier of S by FUNCT_2:def 1;
R is total by NDIFF_1:def 5;
then dom R = the carrier of T by PARTFUN1:def 2;
then
A5: rng L c= dom R;
A6: 0 + K < 1 + K by XREAL_1:8;
A7: now
let e be Real;
assume e > 0;
then
A8: 0/(1 + K) < e/(1 + K) by A2,XREAL_1:74;
set e1=e/(1 + K);
consider d be Real such that
A9: 0 < d and
A10: for h be Point of T st ||.h.|| < d holds ||.R/.h.|| <= e1*||.h.||
by A1,A8,Th7;
set d1=d/( 1 + K );
A11: now
let h be Point of S such that
A12: h <> 0.S and
A13: ||.h.|| < d1;
A14: ||.L.h.|| <= K * ||.h.|| by A3;
A15: ||.h.|| <> 0 by A12,NORMSP_0:def 5;
then
A16: ||.h.|| > 0 by NORMSP_1:4;
then K * ||.h.|| < ( K +1) * ||.h.|| by A6,XREAL_1:68;
then
A17: ||.L.h.|| < ( K +1) * ||.h.|| by A14,XXREAL_0:2;
( K +1) * ||.h.|| < ( K +1) *d1 by A2,A13,XREAL_1:68;
then ||.L.h.|| < ( K +1) * d1 by A17,XXREAL_0:2;
then ||.L.h.|| < d by A2,XCMPLX_1:87;
then
A18: ||.R/.(L.h).|| <= e1*||.L.h.|| by A10;
A19: R/.(L.h) = R/.(L/.h) .=(R*L)/.h by A4,A5,PARTFUN2:5;
e1*||.L.h.|| < e1* ((K +1) * ||.h.||) by A8,A17,XREAL_1:68;
then ||.R/.(L.h).|| < e1* ((K +1) * ||.h.||) by A18,XXREAL_0:2;
then
||.h.||"* ||.(R*L)/.h.|| < ||.h.||"* (e1* ( K +1) * ||.h.||) by A19,A16,
XREAL_1:68;
then ||.h.||"* ||.(R*L)/.h.|| < ||.h.||*||.h.||"*e1* ( K +1);
then ||.h.||"* ||.(R*L)/.h.|| < 1*e1* ( K +1) by A15,XCMPLX_0:def 7;
hence ||.h.||"* ||.(R*L)/.h.|| < e by A2,XCMPLX_1:87;
end;
0/(1 + K) < d/(1 + K) by A2,A9,XREAL_1:74;
hence
ex d1 be Real st d1 > 0 &
for h be Point of S st h <> 0.S & ||.h.|| <
d1 holds ||.h.||"* ||.(R*L)/.h.|| < e by A11;
end;
dom(R*L) = dom L by A5,RELAT_1:27
.= the carrier of S by FUNCT_2:def 1;
then R*L is total by PARTFUN1:def 2;
hence thesis by A7,NDIFF_1:23;
end;
theorem Th9:
for R be RestFunc of S,T for L be Lipschitzian LinearOperator of T,U holds
L*R is RestFunc of S,U
proof
let R be RestFunc of S,T;
let L be Lipschitzian LinearOperator of T,U;
consider K be Real such that
A1: 0 <= K and
A2: for z be Point of T holds ||.L.z.|| <= K * ||.z.|| by LOPBAN_1:def 8;
dom L = the carrier of T by FUNCT_2:def 1;
then
A3: rng R c= dom L;
A4: R is total by NDIFF_1:def 5;
then
A5: dom R = the carrier of S by PARTFUN1:def 2;
A6: 0 + K < 1 + K by XREAL_1:8;
A7: now
let ee be Real such that
A8: ee > 0;
set e=ee/2;
e > 0 by A8,XREAL_1:215;
then
A9: 0/(1 + K) < e/(1 + K) by A1,XREAL_1:74;
set e1=e/( 1 + K );
R is total by NDIFF_1:def 5;
then consider d be Real such that
A10: 0 < d and
A11: for h be Point of S st h <> 0.S & ||.h.|| < d holds ||.h.||"* ||.
R/.h.|| < e1 by A9,NDIFF_1:23;
A12: e < ee by A8,XREAL_1:216;
now
let h be Point of S such that
A13: h <> 0.S and
A14: ||.h.|| < d;
||.h.||"* ||.(R/.h).|| < e1 by A11,A13,A14;
then ( K +1) *( ||.h.||"* ||.R/.h.||) <=( K +1) *e1 by A1,XREAL_1:64;
then
A15: ( K +1) *( ||.h.||"* ||.R/.h.||) <=e by A1,XCMPLX_1:87;
||.h.|| <> 0 by A13,NORMSP_0:def 5;
then
A16: ||.h.|| > 0 by NORMSP_1:4;
0 <= ||.R/.h.|| by NORMSP_1:4;
then
A17: K * ||.R/.h.|| <= ( K +1) * ||.R/.h.|| by A6,XREAL_1:64;
||.L.(R/.h).|| <= K * ||.R/.h.|| by A2;
then ||.L.(R/.h).|| <= ( K +1) * ||.R/.h.|| by A17,XXREAL_0:2;
then
||.h.||"* ||.L.(R/.h).|| <= ||.h.||"*(( K +1) * ||.R/.h.|| ) by A16,
XREAL_1:64;
then
A18: ||.h.||"* ||.L.(R/.h).|| <= e by A15,XXREAL_0:2;
L.(R/.h) = L/.(R/.h) .=(L*R)/.h by A5,A3,PARTFUN2:5;
hence ||.h.||"* ||.(L*R)/.h.|| < ee by A12,A18,XXREAL_0:2;
end;
hence
ex d be Real st d > 0 &
for h be Point of S st h <> 0.S & ||.h.|| < d
holds ||.h.||"* ||.(L*R)/.h.|| < ee by A10;
end;
dom(L*R) = dom R by A3,RELAT_1:27
.= the carrier of S by A4,PARTFUN1:def 2;
then L*R is total by PARTFUN1:def 2;
hence thesis by A7,NDIFF_1:23;
end;
theorem
for R1 be RestFunc of S,T st R1/.0.S=0.T
for R2 be RestFunc of T,U st R2/.0.T=0.U holds R2*R1 is RestFunc of S,U
proof
let R1 be RestFunc of S,T such that
A1: R1/.0.S=0.T;
let R2 be RestFunc of T,U such that
A2: R2/.0.T=0.U;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
then
A3: rng R1 c= dom R2;
A4: R1 is total by NDIFF_1:def 5;
then
A5: dom R1 = the carrier of S by PARTFUN1:def 2;
A6: now
consider d1 be Real such that
A7: 0 < d1 and
A8: for h be Point of S st ||.h.|| < d1 holds ||.R1/.h.|| <=1* ||.h
.|| by A1,Th7;
let e0 be Real such that
A9: e0 > 0;
set e=e0/2;
A10: e < e0 by A9,XREAL_1:216;
e > 0 by A9,XREAL_1:215;
then consider d2 be Real such that
A11: 0 < d2 and
A12: for z be Point of T st ||.z.|| < d2 holds ||.R2/.z.|| <= e*||.z
.|| by A2,Th7;
set d=min(d1,d2);
A13: d <=d2 by XXREAL_0:17;
A14: d <=d1 by XXREAL_0:17;
A15: now
let h be Point of S such that
A16: h <> 0.S and
A17: ||.h.|| < d;
||.h.|| < d1 by A14,A17,XXREAL_0:2;
then
A18: ||.R1/.h.|| <=1* ||.h.|| by A8;
then ||.R1/.h.|| < d by A17,XXREAL_0:2;
then ||.R1/.h.|| < d2 by A13,XXREAL_0:2;
then
A19: ||.R2/.(R1/.h).|| <= e*||.R1/.h.|| by A12;
e*||.R1/.h.|| <= e* ||.h.|| by A9,A18,XREAL_1:64;
then
A20: ||.R2/.(R1/.h).|| <= e*||.h.|| by A19,XXREAL_0:2;
A21: ||.h.|| <> 0 by A16,NORMSP_0:def 5;
then ||.h.|| > 0 by NORMSP_1:4;
then ||.h.||"* ||.R2/.(R1/.h).|| <= ||.h.||"*(e*||.h.||) by A20,
XREAL_1:64;
then ||.h.||"* ||.R2/.(R1/.h).|| <= ||.h.||"*||.h.||*e;
then
A22: ||.h.||"* ||.R2/.(R1/.h).|| <= 1*e by A21,XCMPLX_0:def 7;
R2/.(R1/.h) =(R2*R1)/.h by A5,A3,PARTFUN2:5;
hence ||.h.||"* ||.(R2*R1)/.h.|| < e0 by A10,A22,XXREAL_0:2;
end;
0 < d by A11,A7,XXREAL_0:15;
hence
ex d be Real st d > 0 &
for h be Point of S st h <> 0.S & ||.h.|| < d
holds ||.h.||"* ||.(R2*R1)/.h.|| < e0 by A15;
end;
dom(R2*R1) = dom R1 by A3,RELAT_1:27
.= the carrier of S by A4,PARTFUN1:def 2;
then R2*R1 is total by PARTFUN1:def 2;
hence thesis by A6,NDIFF_1:23;
end;
theorem Th11:
for R1 be RestFunc of S,T st R1/.0.S=0.T for R2 be RestFunc of T,U st R2
/.0.T=0.U for L be Lipschitzian LinearOperator of S,T holds
R2*(L+R1) is RestFunc of S,U
proof
let R1 be RestFunc of S,T;
assume R1/.0.S=0.T;
then consider d0 be Real such that
A1: 0 < d0 and
A2: for h be Point of S st ||.h.|| < d0 holds ||.R1/.h.|| <=1* ||.h.|| by Th7;
let R2 be RestFunc of T,U such that
A3: R2/.0.T=0.U;
let L be Lipschitzian LinearOperator of S,T;
consider K be Real such that
A4: 0 <= K and
A5: for h be Point of S holds ||.L.h.|| <= K * ||.h.|| by LOPBAN_1:def 8;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
then
A6: rng (L+R1) c= dom R2;
R1 is total by NDIFF_1:def 5;
then
A7: L+R1 is total by VFUNCT_1:32;
then
A8: dom(L+R1)=the carrier of S by PARTFUN1:def 2;
A9: now
let ee be Real such that
A10: ee > 0;
set e=ee/2;
A11: e < ee by A10,XREAL_1:216;
set e1=e/( 1 + K );
e > 0 by A10,XREAL_1:215;
then 0/(1 + K) < e/(1 + K) by A4,XREAL_1:74;
then consider d be Real such that
A12: 0 < d and
A13: for z be Point of T st ||.z.|| < d holds ||.R2/.z.|| <= e1*||.z
.|| by A3,Th7;
set d1=d/( 1 + K );
set dd1=min(d0,d1);
A14: dd1 <=d1 by XXREAL_0:17;
A15: dd1 <=d0 by XXREAL_0:17;
A16: now
let h be Point of S such that
A17: h <> 0.S and
A18: ||.h.|| < dd1;
||.h.|| < d0 by A15,A18,XXREAL_0:2;
then
A19: ||.R1/.h.|| <=1* ||.h.|| by A2;
||.L.h.|| <= K * ||.h.|| by A5;
then ||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.|| & ||.L.h.|| + ||.R1/.h
.|| <= K * ||.h.|| + 1* ||.h.|| by A19,NORMSP_1:def 1,XREAL_1:7;
then
A20: ||.L.h+R1/.h.|| <= ( K +1) * ||.h.|| by XXREAL_0:2;
||.h.|| < d1 by A14,A18,XXREAL_0:2;
then ( K +1) * ||.h.|| < ( K +1) *d1 by A4,XREAL_1:68;
then ||.L.h+R1/.h.|| < ( K +1) * d1 by A20,XXREAL_0:2;
then ||.L.h+R1/.h.|| < d by A4,XCMPLX_1:87;
then
A21: ||.R2/.(L.h+R1/.h).|| <= e1*||.L.h+R1/.h.|| by A13;
e1*||.L.h+R1/.h.|| <= e1* ((K +1) * ||.h.||) by A4,A10,A20,XREAL_1:64;
then
A22: ||.R2/.(L.h+R1/.h).|| <= e1* ((K +1) * ||.h.||) by A21,XXREAL_0:2;
A23: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h) .=R2/.((L+R1)/.h) by A8,VFUNCT_1:def 1
.=(R2*(L+R1))/.h by A8,A6,PARTFUN2:5;
A24: ||.h.|| <> 0 by A17,NORMSP_0:def 5;
then ||.h.|| > 0 by NORMSP_1:4;
then
||.h.||"* ||.(R2*(L+R1))/.h.|| <= ||.h.||"* (e1* ( K +1) * ||.h .||
) by A23,A22,XREAL_1:64;
then ||.h.||"* ||.(R2*(L+R1))/.h.|| <= ||.h.||*||.h.||"*e1* ( K +1);
then ||.h.||"* ||.(R2*(L+R1))/.h.|| <= 1*e1* ( K +1) by A24,
XCMPLX_0:def 7;
then ||.h.||"* ||.(R2*(L+R1))/.h.|| <= e by A4,XCMPLX_1:87;
hence ||.h.||"* ||.(R2*(L+R1))/.h.|| < ee by A11,XXREAL_0:2;
end;
0/(1 + K) < d/(1 + K) by A4,A12,XREAL_1:74;
then 0 < dd1 by A1,XXREAL_0:15;
hence
ex dd1 be Real st
dd1 > 0 & for h be Point of S st h <> 0.S & ||.h.||
< dd1 holds ||.h.||"* ||.(R2*(L+R1))/.h.|| < ee by A16;
end;
dom (R2*(L+R1)) = dom(L+R1) by A6,RELAT_1:27
.=the carrier of S by A7,PARTFUN1:def 2;
then R2*(L+R1) is total by PARTFUN1:def 2;
hence thesis by A9,NDIFF_1:23;
end;
theorem Th12:
for R1 be RestFunc of S,T st R1/.0.S=0.T for R2 be RestFunc of T,U st R2
/.0.T=0.U for L1 be Lipschitzian LinearOperator of S,T
for L2 be Lipschitzian
LinearOperator of T,U holds L2*R1+ R2*(L1+R1) is RestFunc of S,U
proof
let R1 be RestFunc of S,T such that
A1: R1/.0.S=0.T;
let R2 be RestFunc of T,U such that
A2: R2/.0.T=0.U;
let L1 be Lipschitzian LinearOperator of S,T;
let L2 be Lipschitzian LinearOperator of T,U;
A3: L2*R1 is RestFunc of S,U by Th9;
R2*(L1+R1) is RestFunc of S,U by A1,A2,Th11;
hence thesis by A3,NDIFF_1:28;
end;
theorem
for f1 be PartFunc of S,T st f1 is_differentiable_in x0 for f2 be
PartFunc of T,U st f2 is_differentiable_in (f1/.x0) holds f2*f1
is_differentiable_in x0 & diff(f2*f1,x0) = diff(f2,f1/.x0)*diff(f1,x0)
proof
let f1 be PartFunc of S,T such that
A1: f1 is_differentiable_in x0;
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f1 and
A3: ex R1 be RestFunc of S,T st R1/.0.S=0.T & R1 is_continuous_in 0.S & for
x be Point of S st x in N1 holds f1/.x-f1/.x0 = diff(f1,x0).(x-x0) + R1/.(x-x0)
by A1,NDIFF_1:47;
let f2 be PartFunc of T,U;
assume f2 is_differentiable_in f1/.x0;
then consider N2 being Neighbourhood of f1/.x0 such that
A4: N2 c= dom f2 and
A5: ex R2 be RestFunc of T,U st R2/.0.T=0.U & R2 is_continuous_in 0.T & for
y be Point of T st y in N2 holds f2/.y-f2/.(f1/.x0) = diff(f2,f1/.x0).(y-f1/.x0
) + R2/.(y-f1/.x0) by NDIFF_1:47;
consider R2 be RestFunc of T,U such that
A6: R2/.0.T=0.U and
A7: for y be Point of T st y in N2 holds f2/.y-f2/.(f1/.x0) = diff(f2,
f1 /.x0).(y-f1/.x0) + R2/.(y-f1/.x0) by A5;
set L2=modetrans(diff(f2,f1/.x0),T,U);
set L1=modetrans(diff(f1,x0),S,T);
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider LB1 = diff(f1,x0) as Element of BoundedLinearOperators(S,T);
R_NormSpace_of_BoundedLinearOperators(T,U) = NORMSTR (#
BoundedLinearOperators(T,U), Zero_(BoundedLinearOperators(T,U),
R_VectorSpace_of_LinearOperators(T,U)), Add_(BoundedLinearOperators(T,U),
R_VectorSpace_of_LinearOperators(T,U)), Mult_(BoundedLinearOperators(T,U),
R_VectorSpace_of_LinearOperators(T,U)), BoundedLinearOperatorsNorm(T,U) #) by
LOPBAN_1:def 14;
then reconsider
LB2 = diff(f2,f1/.x0) as Element of BoundedLinearOperators(T,U);
consider R1 be RestFunc of S,T such that
A8: R1/.0.S=0.T and
A9: for x be Point of S st x in N1 holds f1/.x-f1/.x0 = diff(f1,x0).(x-
x0) + R1/.(x-x0) by A3;
f1 is_continuous_in x0 by A1,NDIFF_1:44;
then consider N3 be Neighbourhood of x0 such that
A10: f1.:N3 c= N2 by NFCONT_1:10;
reconsider R0=L2*R1+R2*(L1+R1) as RestFunc of S,U by A8,A6,Th12;
consider N be Neighbourhood of x0 such that
A11: N c= N1 and
A12: N c= N3 by NDIFF_1:1;
A13: N c= dom (f2*f1)
proof
let x be object;
assume
A14: x in N;
then reconsider x9 = x as Point of S;
A15: x in N1 by A11,A14;
then f1.x9 in f1.:N3 by A2,A12,A14,FUNCT_1:def 6;
then f1.x9 in N2 by A10;
hence thesis by A2,A4,A15,FUNCT_1:11;
end;
A16: LB1=modetrans(LB1,S,T) & LB2=modetrans(LB2,T,U) by LOPBAN_1:def 11;
A17: now
let x be Point of S such that
A18: x in N;
A19: f1/.x-f1/.x0 = diff(f1,x0).(x-x0) + R1/.(x-x0) by A9,A11,A18;
x in N1 by A11,A18;
then f1.x in f1.:N3 by A2,A12,A18,FUNCT_1:def 6;
then
A20: f1.x in N2 by A10;
x in N1 by A11,A18;
then
A21: f1/.x in N2 by A2,A20,PARTFUN1:def 6;
dom L1 = the carrier of S by FUNCT_2:def 1;
then
A22: L2.(L1.(x-x0)) =(diff(f2,f1/.x0)*diff(f1,x0)).(x-x0) by FUNCT_1:13;
A23: x0 in N by NFCONT_1:4;
A24: R1 is total by NDIFF_1:def 5;
then
A25: dom R1 = the carrier of S by PARTFUN1:def 2;
dom L2 = the carrier of T by FUNCT_2:def 1;
then
A26: rng R1 c= dom L2;
then
A27: dom(L2*R1) = dom R1 by RELAT_1:27
.= the carrier of S by A24,PARTFUN1:def 2;
A28: L1+R1 is total by A24,VFUNCT_1:32;
then
A29: dom(L1+R1)=the carrier of S by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
then
A30: rng (L1+R1) c= dom R2;
then dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27
.=the carrier of S by A28,PARTFUN1:def 2;
then
A31: dom (L2*R1+R2*(L1+R1)) = (the carrier of S) /\ (the carrier of S) by A27,
VFUNCT_1:def 1
.= the carrier of S;
A32: L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0))
.=(L2*R1)/.(x-x0) by A25,A26,PARTFUN2:5;
A33: R2/.(L1.(x-x0)+R1/.(x-x0)) = R2/.(L1/.(x-x0)+R1/.(x-x0))
.=R2/.((L1+R1)/.(x-x0)) by A29,VFUNCT_1:def 1
.=(R2*(L1+R1))/.(x-x0) by A29,A30,PARTFUN2:5;
thus (f2*f1)/.x-(f2*f1)/.x0 =f2/.(f1/.x) -(f2*f1)/.x0 by A13,A18,PARTFUN2:3
.=f2/.(f1/.x) -f2/.(f1/.x0) by A13,A23,PARTFUN2:3
.=diff(f2,f1/.x0).(f1/.x-f1/.x0) + R2/.(f1/.x-f1/.x0) by A7,A21
.=L2.(L1.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A16,A19,A33,
VECTSP_1:def 20
.=L2.(L1.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A32,
RLVECT_1:def 3
.=(diff(f2,f1/.x0)*diff(f1,x0)).(x-x0) + R0/.(x-x0) by A31,A22,
VFUNCT_1:def 1;
end;
hence f2*f1 is_differentiable_in x0 by A13,NDIFF_1:def 6;
hence thesis by A13,A17,NDIFF_1:def 7;
end;