:: Differentiable Functions on Normed Linear Spaces :: by Yasunari Shidama :: :: Received June 2, 2011 :: Copyright (c) 2011-2018 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, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1, FUNCT_4, NAT_1, FDIFF_1, SUBSET_1, SEQ_4, RELAT_1, GLIB_000, LOPBAN_1, ORDINAL4, RFINSEQ, 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, GROUP_2, FUNCOP_1, MEMBERED, FINSEQ_5, XXREAL_2, XBOOLE_0, CARD_3, FINSEQ_1, FINSEQ_2, AFINSQ_1, RLVECT_1, SQUARE_1, RVSUM_1, XXREAL_1, PDIFF_1, PRVECT_1, PRVECT_2, ALGSTR_0, EUCLID, CFCONT_1, RFINSEQ2, NORMSP_0, MONOID_0, RLTOPSP1, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, MEMBERED, VALUED_0, COMPLEX1, NAT_D, XXREAL_2, CARD_3, FINSEQ_1, VALUED_1, FINSEQ_2, SEQ_1, SEQ_2, RVSUM_1, RFINSEQ, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, FINSEQ_5, FINSEQ_7, RFINSEQ2, STRUCT_0, MONOID_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, NORMSP_1, VFUNCT_1, EUCLID, LOPBAN_1, PRVECT_1, NFCONT_1, NDIFF_1, PRVECT_2, NFCONT_3, NDIFF_3, RLTOPSP1, FUNCT_7; constructors REAL_1, SQUARE_1, SEQ_2, FDIFF_1, NFCONT_1, RSSPACE, VFUNCT_1, NDIFF_1, RELSET_1, FINSEQ_7, FINSEQ_5, RVSUM_1, BINOP_2, PRVECT_2, RLVECT_2, NAT_D, FINSEQOP, RFINSEQ, RFINSEQ2, SEQ_4, FCONT_1, NFCONT_3, NDIFF_3, MONOID_0, RLTOPSP1, FUNCT_7, COMSEQ_2, FUNCT_4, NUMBERS, RCOMP_1; registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, FUNCT_1, NDIFF_1, FUNCT_2, NUMBERS, XBOOLE_0, VALUED_0, PRVECT_2, FINSEQ_2, FINSEQ_1, CARD_3, NORMSP_0, NORMSP_1, RELAT_1, XXREAL_0, LOPBAN_1, LOPBAN_2, PRVECT_3, FUNCOP_1, NAT_1, FINSEQ_5, XXREAL_2, RCOMP_1, VALUED_1, FDIFF_1, NFCONT_3, FINSET_1, XCMPLX_0, PARTFUN1, CARD_1, MONOID_0, FUNCT_4, SQUARE_1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TARSKI, FUNCT_2, MONOID_0, SUBSET_1; equalities RLVECT_1, LOPBAN_1, EUCLID, RFINSEQ2, FINSEQ_1, FINSEQ_2, STRUCT_0, ALGSTR_0, NORMSP_0, RCOMP_1, XCMPLX_0, SUBSET_1; expansions TARSKI, FUNCT_2, LOPBAN_1, FINSEQ_1, STRUCT_0, SUBSET_1; 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, FUNCT_3, FINSEQ_4, RLVECT_2, FINSEQ_3, ORDINAL1, FINSEQ_1, CARD_3, FUNCT_4, SEQ_4, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, VALUED_0, VECTSP_1, NORMSP_0, XREAL_0, RCOMP_1, FINSEQ_2, FINSEQ_7, RVSUM_1, SQUARE_1, PRVECT_1, PRVECT_2, PDIFF_7, EUCLID, XXREAL_2, FINSEQ_5, NAT_D, RFINSEQ2, INTEGRA5, FCONT_1, NAT_2, NFCONT_3, NDIFF_2, NDIFF_3, CARD_1, ROLLE, XXREAL_1, RLTOPSP1, FUNCT_7, SUBSET_1; schemes FUNCT_2, SEQ_1, FINSEQ_1, NAT_1, FINSEQ_2; begin :: Preliminaries reserve j for set; reserve p,r for Real; reserve S,T,F for RealNormSpace; reserve x0 for Point of S; reserve g for PartFunc of S,T; reserve c for constant sequence of S; reserve R for RestFunc of S,T; reserve G for RealNormSpace-Sequence; reserve i for Element of dom G; reserve f for PartFunc of product G,F; reserve x for Element of product G; theorem Th1: for R be Function of REAL,S holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |.z.|"* ||. R/.z .|| < r proof let R be Function of REAL,S; A1:dom R = REAL by PARTFUN1:def 2; A2:now assume A3: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r); then consider r be Real such that A4: r > 0 and A5: for d be Real st d > 0 holds ex z be Real st z <> 0 & |. z .| < d & not |. z .|"* ||. R/.z .|| < r; defpred P[Nat,Real] means \$2 <> 0 & |. \$2 .| < (1/(\$1+1)) & not |. \$2 .|"* ||. R/.\$2 .|| < r; A6: for n be Element of NAT ex z be Element of REAL st P[n,z] proof let n be Element of NAT; set d = 1/(n + 1); consider z be Real such that A7: z <> 0 & |. z .| < d & not |. z .|"* ||. R/.z .|| < r by A5; reconsider z as Element of REAL by XREAL_0:def 1; take z; thus thesis by A7; end; consider s be Real_Sequence such that A8: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6); A9: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A8; end; A10: now let p be Real; assume A11: 0 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r by A9,A16,A19; end; now assume A21:for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r; now let s be 0-convergent non-zero Real_Sequence; A22: s is convergent & lim s = 0; A23: now let r be Real; assume r > 0; then consider d be Real such that A24: d > 0 and A25: for z be Real st z <> 0 & |.z.| < d holds |.z.|"* ||. R/.z .|| < r by A21; consider n0 be Nat such that A26: for m be Nat st n0 <=m holds |. s.m-0 .| < d by A22,A24,SEQ_2:def 7; take n0; thus for m be Nat st n0 <=m holds ||. ((s")(#)(R/*s)).m- 0.S .|| < r proof A27: rng s c= dom R by A1; let m be Nat; assume n0 <=m; then A28: |. s.m-0 .| < d by A26; A30: m in NAT by ORDINAL1:def 12; |. s.m .|" * ||. R/.(s.m) .|| = |.(s.m)".| * ||. R/.(s.m) .|| by COMPLEX1:66 .= ||. (s.m)"*(R/.(s.m)) .|| by NORMSP_1:def 1 .= ||. (s.m)"*((R/*s).m) .|| by A27,FUNCT_2:109,A30 .= ||. (s".m)*((R/*s).m) .|| by VALUED_1:10 .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2 .= ||. ((s")(#)(R/*s)).m- 0.S .|| by RLVECT_1:13; hence thesis by A25,A28,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.S by A23,NORMSP_1:def 7; end; hence R is RestFunc-like by NDIFF_3:def 1; end; hence thesis by A2; end; theorem Th2: for R be RestFunc of S st R/.0=0.S for e be Real st e > 0 ex d be Real st d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.| proof let R be RestFunc of S such that A1: R/.0=0.S; let e be Real such that A2: e > 0; R is total by NDIFF_3:def 1; then consider d be Real such that A3: d > 0 and A4: for z be Real st z <> 0 & |.z.| < d holds |.z.|"* ||. R/.z .|| < e by A2,Th1; take d; now let h be Real such that A5: |.h.| < d; A6: 0 <= |.h.| by COMPLEX1:46; per cases; suppose A7: h <> 0; then |.h.|"*||. R/.h .|| <= e by A4,A5; then |.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by A6,XREAL_1:64; then A8: |.h.|*|.h.|"*||. R/.h .|| <= e * |.h.|; |.h.| <> 0 by A7,COMPLEX1:45; then 1*||. R/.h .|| <= e * |.h.| by A8,XCMPLX_0:def 7; hence ||. R/.h .|| <= e* |.h.|; end; suppose A9: h = 0; reconsider p0=0 as Real; p0* |.h.| <= e* |.h.| by A2,A6; hence ||. R/.h .|| <= e* |.h.| by A1,A9; end; end; hence thesis by A3; end; theorem Th3: for R be RestFunc of S for L be Lipschitzian LinearOperator of S,T holds L*R is RestFunc of T proof let R be RestFunc of S; let L be Lipschitzian LinearOperator of S,T; consider K be Real such that A1: 0 <= K and A2: for z be Point of S holds ||. L.z .|| <= K * ||.z.|| by LOPBAN_1:def 8; dom L = the carrier of S by FUNCT_2:def 1; then A3:rng R c= dom L; A4:R is total by NDIFF_3:def 1; then A5:dom R = REAL by PARTFUN1:def 2; now let e be Real such that A6: e > 0; set e1 = e/2/(1 + K); consider d be Real such that A7: 0 < d and A8: for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||. R/.h .|| < e1 by A1,A4,A6,Th1; A9: e/2 < e by A6,XREAL_1:216; now let h be Real; reconsider hh=h as Element of REAL by XREAL_0:def 1; assume A10: h <> 0 & |.h.| < d; then |.h.|"* ||.(R/.h).|| < e1 by A8; then (K +1)*(|.h.|"* ||.R/.h.||) <= (K +1)*e1 by A1,XREAL_1:64; then A11: (K +1)*(|.h.|"* ||.R/.h.||) <= e/2 by A1,XCMPLX_1:87; |.h.| <> 0 by A10,COMPLEX1:45; then A12: |.h.| > 0 by COMPLEX1:46; reconsider p0=0, p1=1 as Element of REAL by XREAL_0:def 1; p0 + K < p1 + K by XREAL_1:8; then A13: K * ||.R/.h.|| <= (K +1) * ||.R/.h.|| by XREAL_1:64; ||.L.(R/.h).|| <= K * ||.R/.h.|| by A2; then ||.L.(R/.h).|| <= (K +1) * ||.R/.h.|| by A13,XXREAL_0:2; then |.h.|"* ||.L.(R/.h).|| <= |.h.|"*((K +1)*||. R/.h .||) by A12,XREAL_1:64 ; then A14: |.h.|"* ||.L.(R/.h).|| <= e/2 by A11,XXREAL_0:2; L.(R/.h) = L/.(R/.h); then L.(R/.hh) =(L*R)/.hh by A5,A3,PARTFUN2:5; hence |.h.|"* ||.(L*R)/.h.|| < e by A9,A14,XXREAL_0:2; end; hence ex d be Real st d > 0 & for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||.(L*R)/.h.|| < e by A7; end; hence thesis by A4,Th1; end; theorem Th4: for R1 be RestFunc of S st R1/.0 = 0.S for R2 be RestFunc of S,T st R2/.(0.S) = 0.T for L be LinearFunc of S holds R2*(L+R1) is RestFunc of T proof let R1 be RestFunc of S; assume R1/.0 = 0.S; then consider d0 be Real such that A1: 0 < d0 and A2: for h be Real st |.h.| < d0 holds ||.R1/.h.|| <= 1* |.h.| by Th2; let R2 be RestFunc of S,T such that A3:R2/.(0.S) = 0.T; let L be LinearFunc of S; consider r be Point of S such that A4: for h be Real holds L/.h = h*r by NDIFF_3:def 2; reconsider K = ||.r.|| as Real; R2 is total by NDIFF_1:def 5; then dom R2 = the carrier of S by PARTFUN1:def 2; then A5:rng(L+R1) c= dom R2; R1 is total by NDIFF_3:def 1; then L+R1 is total by VFUNCT_1:32; then A6:dom(L+R1) = REAL by PARTFUN1:def 2; then dom(R2*(L+R1)) = REAL by A5,RELAT_1:27; then A7:R2*(L+R1) is total by PARTFUN1:def 2; now let e be Real such that A8: e > 0; A9: e/2 < e by A8,XREAL_1:216; set e1 = e/2/(1 + K); consider d be Real such that A10: 0 < d and A11: for z be Point of S st ||.z.|| < d holds ||.R2/.z.|| <= e1*||.z.|| by A3,A8,NDIFF_2:7; set d1 = d/(1 + K); set dd1 = min(d0,d1); A12: dd1 <= d1 & dd1 <= d0 by XXREAL_0:17; A13: now let hh be Real such that A14: hh <> 0 and A15: |.hh.| < dd1; reconsider h=hh as Element of REAL by XREAL_0:def 1; |.h.| < d0 by A12,A15,XXREAL_0:2; then A16: ||.R1/.h.|| <=1* |.h.| by A2; reconsider p0=0 as Element of REAL by XREAL_0:def 1; L.h = L/.h .= h*r by A4; then ||. L.h .|| - K * |.h.| + K * |.h.| <= p0 + K * |.h.| by NORMSP_1:def 1; then ||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.|| & ||.L.h.|| + ||. R1/.h .|| <= K * |.h.| + 1 * |.h.| by A16,NORMSP_1:def 1,XREAL_1:7; then A17: ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2; then A18: e1 * ||. L.h+R1/.h .|| <= e1*((K +1)*|.h.|) by A8,XREAL_1:64; |.h.| < d1 by A12,A15,XXREAL_0:2; then (K +1) * |.h.| < (K +1) * d1 by XREAL_1:68; then ||. L.h+R1/.h .|| < (K +1) * d1 by A17,XXREAL_0:2; then ||. L.h+R1/.h.|| < d by XCMPLX_1:87; then ||. R2/.(L.h+R1/.h) .|| <= e1 * ||. L.h+R1/.h .|| by A11; then A19: ||. R2/.(L.h+R1/.h) .|| <= e1*((K +1)*|.h.|) by A18,XXREAL_0:2; A20: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h) .=R2/.((L+R1)/.h) by A6,VFUNCT_1:def 1 .=(R2*(L+R1))/.h by A6,A5,PARTFUN2:5; A21: |.h.| <> 0 by A14,COMPLEX1:45; then |.h.| > 0 by COMPLEX1:46; then |.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* (K +1) * |.h.|) by A20,A19,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 A21,XCMPLX_0:def 7; then |.h.|"* ||. (R2*(L+R1))/.h .|| <= e/2 by XCMPLX_1:87; hence |.hh.|"* ||.(R2*(L+R1))/.hh.|| < e by A9,XXREAL_0:2; end; 0 < dd1 by A1,A10,XXREAL_0:15; hence ex dd1 be Real st dd1 > 0 & for h be Real st h <> 0 & |.h.| < dd1 holds |.h.|"* ||. (R2*(L+R1))/.h .|| < e by A13; end; hence thesis by A7,Th1; end; theorem Th5: for R1 be RestFunc of S st R1/.0=0.S for R2 be RestFunc of S,T st R2/.(0.S)=0.T for L1 be LinearFunc of S for L2 be Lipschitzian LinearOperator of S,T holds L2*R1 + R2*(L1+R1) is RestFunc of T proof let R1 be RestFunc of S such that A1: R1/.0=0.S; let R2 be RestFunc of S,T such that A2: R2/.(0.S)=0.T; let L1 be LinearFunc of S; let L2 be Lipschitzian LinearOperator of S,T; L2*R1 is RestFunc of T & R2*(L1+R1) is RestFunc of T by A1,A2,Th4,Th3; hence thesis by NDIFF_3:7; end; reconsider jj=1 as Element of REAL by XREAL_0:def 1; theorem Th6: for x0 be Real for g be PartFunc of REAL,the carrier of S st g is_differentiable_in x0 for f be PartFunc of the carrier of S,the carrier of T st f is_differentiable_in (g/.x0) holds f*g is_differentiable_in x0 & diff(f*g,x0) = diff(f,g/.x0).diff(g,x0) proof let x0 be Real; let g be PartFunc of REAL,the carrier of S such that A1: g is_differentiable_in x0; consider N1 being Neighbourhood of x0 such that A2: N1 c= dom g and A3: ex L1 be LinearFunc of S,R1 be RestFunc of S st diff(g,x0) = L1/.1 & for x be Real st x in N1 holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A1,NDIFF_3:def 4; let f be PartFunc of the carrier of S,the carrier of T; assume f is_differentiable_in g/.x0; then consider N2 being Neighbourhood of g/.x0 such that A4: N2 c= dom f and A5: ex R2 be RestFunc of S,T st R2/.(0.S) = 0.T & R2 is_continuous_in 0.S & for y be Point of S st y in N2 holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by NDIFF_1:47; consider R2 be RestFunc of S,T such that A6: R2/.0.S=0.T and A7: for y be Point of S st y in N2 holds f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by A5; reconsider L2 = diff(f,g/.x0) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9; consider L1 be LinearFunc of S,R1 be RestFunc of S such that A8: diff(g,x0) = L1/.1 & for x be Real st x in N1 holds g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A3; consider r be Point of S such that A9: for p be Real holds L1/.p = p*r by NDIFF_3:def 2; reconsider p0=0 as Element of REAL by XREAL_0:def 1; g/.x0-g/.x0 = L1/.(x0-x0) + R1/.(x0-x0) by A8,RCOMP_1:16; then 0.S = L1/.0 + R1/.0 by RLVECT_1:15; then 0.S = p0*r + R1/.0 by A9; then 0.S = 0.S + R1/.0 by RLVECT_1:10; then R1/.0 = 0.S by RLVECT_1:4; then reconsider R0=L2*R1+R2*(L1+R1) as RestFunc of T by A6,Th5; A10: dom(L2*L1) = REAL by FUNCT_2:def 1; reconsider q = L2.r as Point of T; now let pp be Real; reconsider p=pp as Element of REAL by XREAL_0:def 1; L2.(L1/.p) = L2.(p*r) by A9; then L2.(L1/.p) = p*q by LOPBAN_1:def 5; then (L2*L1).p = p*q by A10,FUNCT_1:12; hence (L2*L1)/.pp = pp*q by A10,PARTFUN1:def 6; end; then reconsider L0=L2*L1 as LinearFunc of T by NDIFF_3:def 2; g is_continuous_in x0 by A1,NDIFF_3:22; then consider N3 be Neighbourhood of x0 such that A11: g.:N3 c= N2 by NFCONT_3:10; consider N be Neighbourhood of x0 such that A12: N c= N1 and A13: N c= N3 by RCOMP_1:17; A14: dom L2 = the carrier of S by FUNCT_2:def 1; then A15: rng R1 c= dom L2; A16: rng L1 c= dom L2 by A14; now let x be object; assume A17: x in N; then reconsider x9 = x as Real; A18: x in N1 by A12,A17; then g.x9 in g.:N3 by A2,A13,A17,FUNCT_1:def 6; then g.x9 in N2 by A11; hence x in dom(f*g) by A2,A4,A18,FUNCT_1:11; end; then A19: N c= dom(f*g); A20: now let x be Real such that A21: x in N; A22: g/.x-g/.x0 = L1/.(x-x0) + R1/.(x-x0) by A8,A12,A21; x in N1 by A12,A21; then g.x in g.:N3 by A2,A13,A21,FUNCT_1:def 6; then g.x in N2 by A11; then A24: g/.x in N2 by A2,A12,A21,PARTFUN1:def 6; A25: x0 in N by RCOMP_1:16; A26: R1 is total by NDIFF_3:def 1; then A27: dom R1 = REAL by PARTFUN1:def 2; A28: dom(L2*R1) = REAL by A26,PARTFUN1:def 2; L1+R1 is total by A26,VFUNCT_1:32; then A29: dom(L1+R1)=REAL by PARTFUN1:def 2; R2 is total by NDIFF_1:def 5; then dom R2 = the carrier of S by PARTFUN1:def 2; then A30: rng (L1+R1) c= dom R2; then dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27; then A31: dom (L2*R1+R2*(L1+R1)) = REAL /\ REAL by A28,A29,VFUNCT_1:def 1; reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1; L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0)); then A32: L2.(R1/.(x-x0)) =(L2*R1)/.(dxx0) by A27,A15,PARTFUN2:5; A33: R2/.(L1/.(x-x0)+R1/.(x-x0)) =R2/.((L1+R1)/.(dxx0)) by A29,VFUNCT_1:def 1 .=(R2*(L1+R1))/.(dxx0) by A29,A30,PARTFUN2:5; A34: dom L1 = REAL by FUNCT_2:def 1; A35: (L2*L1)/.(x-x0) = L2/.(L1/.(dxx0)) by PARTFUN2:5,A34,A16; thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A19,A21,PARTFUN2:3 .=f/.(g/.x) -f/.(g/.x0) by A19,A25,PARTFUN2:3 .=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A24 .=L2.(L1/.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A22,A33, VECTSP_1:def 20 .=L2.(L1/.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A32, RLVECT_1:def 3 .=L0/.(x-x0) + R0/.(x-x0) by A35,A31,VFUNCT_1:def 1; end; hence A36: f*g is_differentiable_in x0 by A19,NDIFF_3:def 3; dom L1 = REAL by FUNCT_2:def 1; then (L2*L1)/.1 = L2/.(L1/.jj) by PARTFUN2:5,A16 .= diff(f,g/.x0).diff(g,x0) by A8; hence thesis by A36,A19,A20,NDIFF_3:def 4; end; theorem Th7: for S be RealNormSpace, xseq be FinSequence of S, yseq be FinSequence of REAL st len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ) holds ||.Sum xseq.|| <= Sum yseq proof let S be RealNormSpace, xseq be FinSequence of S, yseq be FinSequence of REAL; assume that A1: len xseq = len yseq and A2: for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .||; defpred P[Nat] means for xseq be FinSequence of S, yseq be FinSequence of REAL st \$1=len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ) holds ||.Sum xseq.|| <= Sum yseq; A3:P[0] proof let xseq be FinSequence of S, yseq be FinSequence of REAL; assume A4: 0 = len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ); consider Sx be sequence of the carrier of S such that A5: Sum xseq = Sx.(len xseq) & Sx.0 = 0.S & for j be Nat, v be Element of S st j < len xseq & v = xseq.(j+1) holds Sx.(j+1) = Sx.j + v by RLVECT_1:def 12; yseq = {} by A4; hence thesis by A4,A5,RVSUM_1:72; end; A6:now let i be Nat; assume A7: P[i]; now let xseq be FinSequence of S, yseq be FinSequence of REAL; set xseq0=xseq|i, yseq0=yseq|i; assume A8: i+1=len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ); A9: for k be Element of NAT st k in dom xseq0 holds yseq0.k = ||. xseq0/.k .|| proof let k be Element of NAT; assume A10: k in dom xseq0; then A11: k in Seg i & k in dom xseq by RELAT_1:57; then A12: yseq.k = ||. xseq/.k .|| by A8; xseq/.k = xseq.k by A11,PARTFUN1:def 6; then xseq/.k = xseq0.k by A11,FUNCT_1:49; then xseq/.k = xseq0/.k by A10,PARTFUN1:def 6; hence thesis by A11,A12,FUNCT_1:49; end; A13: dom xseq = Seg(i+1) by A8,FINSEQ_1:def 3; then A14: yseq.(i+1) = ||. xseq/.(i+1) .|| by A8,FINSEQ_1:4; A15: 1 <= i + 1 by NAT_1:11; yseq = (yseq|i)^<*yseq/.(i+1) *> by A8,FINSEQ_5:21; then yseq = yseq0 ^<*(yseq.(i+1))*> by A8,A15,FINSEQ_4:15; then A16: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74; reconsider v = xseq.(len xseq) as Element of S by A13,A8,FINSEQ_1:4,PARTFUN1:4; A18: v = xseq/.(i+1) by A8,A13,FINSEQ_1:4,PARTFUN1:def 6; A19: i=len xseq0 by A8,FINSEQ_1:59,NAT_1:11; then xseq0 = xseq| (dom xseq0) by FINSEQ_1:def 3; then A20: Sum xseq = Sum xseq0 + v by A8,A19,RLVECT_1:38; A21: ||. Sum xseq0 + v.|| <= ||.Sum xseq0 .|| + ||. v .|| by NORMSP_1:def 1; len xseq0 = len yseq0 by A8,A19,FINSEQ_1:59,NAT_1:11; then ||. Sum xseq0 .|| + ||.v.|| <= Sum yseq0 + yseq.(i+1) by A7,A9,A19,A14,A18,XREAL_1:6; hence ||. Sum xseq .|| <= Sum yseq by A16,A20,A21,XXREAL_0:2; end; hence P[i+1]; end; for i be Nat holds P[i] from NAT_1:sch 2(A3,A6); hence thesis by A1,A2; end; theorem Th8: for S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x holds N1/\ N2 is Neighbourhood of x proof let S be RealNormSpace, x be Point of S, N1,N2 be Neighbourhood of x; consider N be Neighbourhood of x such that A1: N c= N1 & N c= N2 by NDIFF_1:1; A2:N c= N1/\ N2 by A1,XBOOLE_1:19; consider g be Real such that A3: 0 < g and A4: {y where y is Point of S: ||.y-x .|| < g} c= N by NFCONT_1:def 1; {y where y is Point of S: ||.y-x .|| < g} c= N1 /\ N2 by A2,A4; hence thesis by A3,NFCONT_1:def 1; end; theorem Th9: for X be non-empty FinSequence, x be set st x in product X holds x is FinSequence proof let X be non-empty FinSequence, x be set; assume x in product X; then consider g be Function such that A1: x = g & dom g = dom X & for i be object st i in dom X holds g.i in X.i by CARD_3:def 5; dom g = Seg len X by A1,FINSEQ_1:def 3; hence x is FinSequence by A1,FINSEQ_1:def 2; end; registration let G be RealNormSpace-Sequence; cluster product G -> constituted-FinSeqs; coherence proof let a be Element of product G; product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hence thesis by Th9; end; end; Lm1: now let G be RealLinearSpace-Sequence; len carr G = len G by PRVECT_2:def 4; hence dom carr G = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; end; definition let G be RealLinearSpace-Sequence; let z be Element of product carr G; let j be Element of dom G; redefine func z.j -> Element of G.j; correctness proof reconsider zz=z as FinSequence by Th9; dom carr G = dom G by Lm1; then zz.j in carr G.j by CARD_3:9; hence thesis by PRVECT_2:def 4; end; end; theorem Th10: the carrier of product G = product carr G proof product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hence thesis; end; theorem Th11: for i be Element of dom G, r be set, x be Function st r in the carrier of (G.i) & x in product carr G holds x +* (i,r) in the carrier of product G proof let i be Element of dom G, r be set, x be Function; assume A1: r in the carrier of (G.i) & x in product carr G; then consider g be Function such that A2: x = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; set h = x +* (i,r); set s = i .--> r; s = {i} --> r by FUNCOP_1:def 9; then A3:dom s = {i} by FUNCOP_1:13; A4:dom h = dom carr G by A2,FUNCT_7:30; for j be object st j in dom carr G holds h.j in (carr G).j proof let j be object; assume A5: j in dom carr G; per cases; suppose not j in dom s; then j <> i by A3,TARSKI:def 1; then h.j = x.j by FUNCT_7:32; hence h.j in (carr G).j by A2,A5; end; suppose j in dom s; then A6: j = i by TARSKI:def 1; then h.j = r by A5,A2,FUNCT_7:31; hence h.j in (carr G).j by A1,A6,PRVECT_2:def 4; end; end; then x +* (i,r) in product carr G by A4,CARD_3:def 5; hence thesis by Th10; end; definition let G be RealNormSpace-Sequence; attr G is non-trivial means :Def1: for j be Element of dom G holds G.j is non trivial; end; registration cluster non-trivial for RealNormSpace-Sequence; correctness proof take G = <* the non trivial RealNormSpace *>; let j be Element of dom G; dom G = Seg 1 by FINSEQ_1:38; then j = 1 by FINSEQ_1:2,TARSKI:def 1; hence thesis by FINSEQ_1:40; end; end; registration let G be non-trivial RealNormSpace-Sequence; let i be Element of dom G; cluster G.i -> non trivial for RealNormSpace; correctness by Def1; end; registration let G be non-trivial RealNormSpace-Sequence; cluster product G -> non trivial; correctness proof A1:the carrier of product G = product carr G by Th10; not for x,y be set st x in product carr G & y in product carr G holds x = y proof assume A2: for x,y be set st x in product carr G & y in product carr G holds x = y; consider z be object such that A3: z in product carr G by XBOOLE_0:def 1; consider g be Function such that A4: z = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by A3,CARD_3:def 5; set i = the Element of dom G; now let r,s be object; assume A5: r in the carrier of (G.i) & s in the carrier of (G.i); g +* (i,r) in the carrier of product G & g +* (i,s) in the carrier of product G by Th11,A3,A4,A5; then g +* (i,r) in product carr G & g +* (i,s) in product carr G by Th10; then A6: g +* (i,r) = g +* (i,s) by A2; i in dom G; then A7: i in dom g by A4,Lm1; then (g +* (i,r)).i = r by FUNCT_7:31; hence r=s by A6,A7,FUNCT_7:31; end; hence contradiction by ZFMISC_1:def 10; end; hence thesis by A1; end; end; theorem Th12: for G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G st p=p0 & q=q0 holds p+q = r0 iff for i be Element of dom G holds r0.i = p0.i + q0.i proof let G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G; assume A1: p=p0 & q=q0; len carr G = len G by PRVECT_2:def 4; then A2:dom carr G = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; A3: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hereby assume A4: p+q = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by A2; (addop G).i0 = the addF of (G.i0) by PRVECT_2:def 5; hence r0.i = p0.i + q0.i by A1,A4,A3,PRVECT_1:def 8; end; end; assume A5: for i be Element of dom G holds r0.i = p0.i + q0.i; reconsider pq=p+q as Element of product carr G by Th10; A6:ex g be Function st pq = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A7:ex g be Function st r0 = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be object; assume A8: i0 in dom pq; then reconsider i1=i0 as Element of dom G by A2,A6; reconsider i =i0 as Element of dom carr G by A8,A6; (addop G).i = the addF of (G.i) by PRVECT_2:def 5; then pq.i0 = p0.i1 + q0.i1 by A1,A3,PRVECT_1:def 8; hence pq.i0 = r0.i0 by A5; end; hence p+q = r0 by A6,A7,FUNCT_1:2; end; theorem Th13: for G be RealNormSpace-Sequence, p be Point of product G, r be Real, r0,p0 be Element of product carr G st p=p0 holds r*p = r0 iff for i be Element of dom G holds r0.i = r*(p0.i) proof let G be RealNormSpace-Sequence, p be Point of product G, r be Real, r0,p0 be Element of product carr G; assume A1: p=p0; hereby assume A2: r*p = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by Lm1; A3: (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8; reconsider rr=r as Element of REAL by XREAL_0:def 1; product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; hence r0.i = rr*(p0.i) by A1,A2,A3,PRVECT_2:def 2 .= r*(p0.i); end; end; assume A4: for i be Element of dom G holds r0.i = r* (p0.i); reconsider rp = r*p as Element of product carr G by Th10; A5:ex g be Function st rp = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A6:ex g be Function st r0 = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be object; assume A7: i0 in dom rp; then reconsider i1=i0 as Element of dom G by Lm1,A5; reconsider i=i0 as Element of dom carr G by A7,A5; A8: product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; reconsider r as Element of REAL by XREAL_0:def 1; (multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then rp.i0 = r*(p0.i1) by A1,A8,PRVECT_2:def 2; hence rp.i0 = r0.i0 by A4; end; hence r*p = r0 by A5,A6,FUNCT_1:2; end; theorem Th14: for G be RealNormSpace-Sequence, p0 be Element of product carr G holds 0.(product G)=p0 iff for i be Element of dom G holds p0.i = 0.(G.i) proof let G be RealNormSpace-Sequence, p0 be Element of product carr G; A1:dom carr G = dom G by Lm1; A2:product G = NORMSTR(# product carr G,zeros G,[:addop G:] ,[:multop G:], productnorm G #) by PRVECT_2:6; hence 0.(product G) = p0 implies for i be Element of dom G holds p0.i = 0.(G.i) by A1,PRVECT_2:def 7; assume A3:for i be Element of dom G holds p0.i = 0.(G.i); now let i0 be Element of dom carr G; reconsider i=i0 as Element of dom G by Lm1; p0.i0 = 0.(G.i) by A3; hence p0.i0 = the ZeroF of (G.i0); end; hence 0.(product G)=p0 by A2,PRVECT_2:def 7; end; theorem Th15: for G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G st p=p0 & q=q0 holds p-q = r0 iff for i be Element of dom G holds r0.i = p0.i - q0.i proof let G be RealNormSpace-Sequence, p,q be Point of product G, r0,p0,q0 be Element of product carr G; assume A1: p=p0 & q=q0; reconsider qq0=(-1)*q as Element of product carr G by Th10; A2:p-q = p+(-1)*q by RLVECT_1:16; hereby assume A3: p-q = r0; thus for i be Element of dom G holds r0.i = p0.i - q0.i proof let i be Element of dom G; A4: r0.i = p0.i + qq0.i by Th12,A3,A1,A2; qq0.i = (-1)*(q0.i) by A1,Th13; hence thesis by A4,RLVECT_1:16; end; end; assume A5: for i be Element of dom G holds r0.i = p0.i - q0.i; now let i be Element of dom G; A6: qq0.i = (-1)*(q0.i) by A1,Th13; r0.i = p0.i - q0.i by A5; hence r0.i = p0.i + qq0.i by A6,RLVECT_1:16; end; hence p-q = r0 by A2,Th12,A1; end; begin :: Mean value theorem for vector-valued functions Lm2: now let S be RealLinearSpace; let p,q be Point of S; let z1 be Real; thus p+z1*(q-p) = p+(z1*q + (z1*(-p))) by RLVECT_1:def 5 .= p+(z1*q+- z1*p) by RLVECT_1:25 .= p+-z1*p+z1*q by RLVECT_1:def 3 .= 1*p-z1*p + z1*q by RLVECT_1:def 8 .= (1-z1)*p + z1*q by RLVECT_1:35; end; notation let S be RealLinearSpace; let p,q be Point of S; synonym [.p,q.] for LSeg(p,q); end; definition let S be RealLinearSpace; let p,q be Point of S; func ]. p,q .[ -> Subset of S equals [.p,q.] \ {p,q}; correctness; end; theorem LMOPN: for S be RealLinearSpace, p,q be Point of S st p <> q holds ].p,q.[ = { p+t*(q-p) where t is Real : 0 < t & t < 1} proof let S be RealLinearSpace, p,q be Point of S; assume AS1: p <> q; set A = { p+t*(q-p) where t is Real : 0 < t & t < 1}; for x be object holds (x in ].p,q.[ iff x in A) proof let x be object; hereby assume x in ].p,q.[; then P1: x in [.p,q.] & not x in {p,q} by XBOOLE_0:def 5; then x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1} by RLTOPSP1:def 2; then consider t be Real such that P2: x= (1-t)*p+t*q & 0 <= t & t <= 1; P3: x= p+t*(q-p) by P2,Lm2; P4: 0 <> t proof assume t = 0; then x = p + 0.S by P3,RLVECT_1:10 .= p by RLVECT_1:4; hence contradiction by P1,TARSKI:def 2; end; 1 <> t proof assume t = 1; then x = p + (q-p) by P3,RLVECT_1:def 8 .= q- (p - p) by RLVECT_1:29 .= q - 0.S by RLVECT_1:15 .= q by RLVECT_1:13; hence contradiction by P1,TARSKI:def 2; end; then 0 < t & t < 1 by P2,P4,XXREAL_0:1; hence x in A by P3; end; assume x in A; then consider t be Real such that P4: x= p+t*(q-p) & 0 < t & t < 1; x= (1-t)*p+t*q by Lm2,P4; then x in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1} by P4; then P5: x in [.p,q.] by RLTOPSP1:def 2; P6: x <> p proof assume x = p; then P7: 0.S = t*(q-p) + p - p by P4,RLVECT_1:15 .= t*(q-p) + (p-p) by RLVECT_1:28 .= t*(q-p) + 0.S by RLVECT_1:15 .= t*(q-p) by RLVECT_1:4; q-p <> 0.S by AS1,RLVECT_1:21; hence contradiction by P4,P7,RLVECT_1:11; end; x <> q proof assume x = q; then q-p = t*(q-p) + (p-p) by P4,RLVECT_1:28 .=t*(q-p) + 0.S by RLVECT_1:15 .=t*(q-p) by RLVECT_1:4; then 1*(q-p) = t*(q-p) by RLVECT_1:def 8; then 1*(q-p) - t*(q-p) =0.S by RLVECT_1:15; then P7: (1-t)* (q-p) = 0.S by RLVECT_1:35; q-p <> 0.S by AS1,RLVECT_1:21; then 1-t = 0 by RLVECT_1:11,P7; hence contradiction by P4; end; then not x in {p,q} by P6,TARSKI:def 2; hence x in ]. p,q .[ by P5,XBOOLE_0:def 5; end; hence thesis by TARSKI:2; end; Lm3: for x be Real st for e be Real st 0 < e holds x <= e holds x <= 0 proof let x be Real; assume A1: for e be Real st 0 < e holds x <= e; assume A2: not x <= 0; then x <= x/2 by A1; then x - (x/2) <= (x/2) - (x/2) by XREAL_1:9; hence contradiction by A2; end; theorem Th17: for T be RealNormSpace, R be PartFunc of REAL,T st R is total holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.| ) < r proof let T be RealNormSpace, R be PartFunc of REAL,T; assume A1: R is total; A2:now assume A3: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/ |.z.|) < r ); then consider r be Real such that A4: r > 0 and A5: for d be Real st d > 0 holds ex z be Real st z <> 0 & |.z.| < d & not ( ||. R/.z .||/ |.z.| ) < r; defpred P[Nat,Element of REAL] means \$2 <> 0 & |.\$2.| < (1/(\$1+1)) & not ( (||. R/.\$2 .||/|.\$2.| ) < r ); A6: now let n be Element of NAT; consider z be Real such that A7: z <> 0 & |.z.| < 1/(n + 1) & not ( ||. R/.z .||/ |.z.| ) < r by A5; reconsider z as Element of REAL by XREAL_0:def 1; take z; thus P[n,z] by A7; end; consider s be Real_Sequence such that A8: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6); A9: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A8; end; A10: now let p be Real; assume A11: 0 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.| ) < r by A9,A16,A19; end; now assume A21: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.|) < r; now let s be 0-convergent non-zero Real_Sequence; A22: s is convergent & lim s = 0; A23: now let r be Real; assume r > 0; then consider d be Real such that A24: d > 0 and A25: for z be Real st z <> 0 & |.z.| < d holds ( ||. R/.z .||/|.z.|) < r by A21; consider n be Nat such that A26: for m be Nat st n <=m holds |.s.m-0 .| < d by A22,A24,SEQ_2:def 7; take n; thus for m be Nat st n <=m holds ||. ((s")(#)(R/*s)).m- 0.T.|| < r proof dom R = REAL by A1,PARTFUN1:def 2; then A27: rng s c= dom R; let m be Nat; A28: m in NAT by ORDINAL1:def 12; assume n <=m; then A29: |.s.m-0 .| < d by A26; ||.(R/.(s.m)).|| / |.s.m.| = |.(s.m)".| * ||.(R/.(s.m)).|| by COMPLEX1:66 .= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1 .= ||.(s.m)"*((R/*s).m).|| by A27,FUNCT_2:109,A28 .= ||.(s".m)*((R/*s).m).|| by VALUED_1:10 .= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2 .= ||. ((s")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13; hence thesis by A25,A29,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.T by A23,NORMSP_1:def 7; end; hence R is RestFunc-like by A1,NDIFF_3:def 1; end; hence thesis by A2; end; theorem Th18: for R be Function of REAL,REAL holds R is RestFunc-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds (|.R.z.|/ |.z.|) < r proof let R be Function of REAL,REAL; A1:now assume A2: R is RestFunc-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( |.R.z.|/ |.z.| ) < r); then consider r be Real such that A3: r > 0 and A4: for d be Real st d > 0 holds ex z be Real st z <> 0 & |.z.| < d & not ( |.R.z.|/|.z.|) < r; defpred P[Nat,Element of REAL] means \$2 <> 0 & |.\$2.| < 1/(\$1+1) & not |.R.\$2.|/|.\$2.| < r; A5: now let n be Element of NAT; consider z be Real such that A6: z <> 0 & |.z.| < 1/(n + 1) & not ( |.R.z.|/|.z.|) < r by A4; reconsider z as Element of REAL by XREAL_0:def 1; take z; thus P[n,z] by A6; end; consider s be Real_Sequence such that A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A5); A8: for n being Nat holds P[n,s.n] proof let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by A7; end; A9: now let p be Real; assume A10: 0 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r by A8,A15,A18; end; now assume A19: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & |.z.| < d holds ( |.R.z.|/|.z.| ) < r; now let s be 0-convergent non-zero Real_Sequence; A20: s is convergent & lim s = 0; A21: now let r be Real; assume A22: r > 0; consider d be Real such that A23: d > 0 and A24: for z be Real st z <> 0 & |.z.| < d holds |.R.z.|/|.z.| < r by A22,A19; consider n be Nat such that A25: for m be Nat st n <= m holds |.s.m-0 .| < d by A20,A23,SEQ_2:def 7; take n; hereby let m be Nat; A26: m in NAT by ORDINAL1:def 12; assume n <=m; then A27: |.s.m-0 .| < d by A25; |.R.(s.m).| / |.s.m.| = |.(s.m)".| * |.R.(s.m).| by COMPLEX1:66 .= |.(s.m)" * R.(s.m).| by COMPLEX1:65 .= |.(s.m)" * (R/*s).m.| by FUNCT_2:115,A26 .= |.s".m * (R/*s).m .| by VALUED_1:10 .= |.(s"(#)(R/*s)).m - 0 .| by SEQ_1:8; hence |. ((s")(#)(R/*s)).m- 0 .| < r by A24,A27,SEQ_1:5; end; end; hence (s")(#)(R/*s) is convergent by SEQ_2:def 6; hence lim((s")(#)(R/*s)) = 0 by A21,SEQ_2:def 7; end; hence R is RestFunc-like by FDIFF_1:def 2; end; hence thesis by A1; end; reconsider jj=1 as Real; Lm4: for T be RealNormSpace, f be PartFunc of REAL,T, g be PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f| [.0,1.] is continuous & g| [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & (for x be Real st x in ].0,1.[ holds ||. diff(f,x) .|| <= diff(g,x)) holds ||. f/.1 -f/.0 .|| <= g/.1 - g/.0 proof let T be RealNormSpace, f be PartFunc of REAL,T, g be PartFunc of REAL,REAL; assume A1: dom f = [.0,1.] & dom g = [.0,1.] & f| [.0,1.] is continuous & g| [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & (for x be Real st x in ].0,1.[ holds ||. diff(f,x) .|| <= diff(g,x)); now let e be Real; assume A2: 0 < e; set e1=e/2; set B = {x where x is Real : x in [.0,1.] & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0}; now let z be object; assume z in B; then ex x be Real st z=x & x in [.0,1.] & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; hence z in REAL; end; then reconsider B as Subset of REAL by TARSKI:def 3; now let r be Real; assume r in B; then ex x be Real st r = x & x in [.0,1.] & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; then A3: ex t be Real st r = t & 0<=t & t<=1; then |.r.| = r by ABSVALUE:def 1; hence |.r.| < 2 by A3,XXREAL_0:2; end; then A4: B is real-bounded by SEQ_4:4; set s = upper_bound B; A5: ex d be Real st 0 < d & d in B proof 0 in [.0,1.]; then consider d1 be Real such that A6: 0 < d1 & for x1 be Real st x1 in [.0,1.] & |.x1-0 .| < d1 holds ||. f/.x1 - f/.0 .|| < e1 by A2,A1,NFCONT_3:17; set d2=d1/2; A7: d2 < d1 by A6,XREAL_1:216; take d = min(d2,1); thus A8: 0 < d by A6,XXREAL_0:21; A9: d <= 1 by XXREAL_0:17; then A10: d in [.0,1.] by A8; A11: d <= d2 by XXREAL_0:17; |.d-0 .| = d by A8,ABSVALUE:def 1; then |.d-0 .| < d1 by A11,A7,XXREAL_0:2; then A12: ||. f/.d - f/.0 .|| < e1 by A6,A10; A13: [.0,d.] c= dom g by A1,A9,XXREAL_1:34; A14: g| [.0,d.] is continuous by A1,A9,FCONT_1:16,XXREAL_1:34; A15: ].0,d.[ c=].0,1.[ by A9,XXREAL_1:46; then consider x0 be Real such that A16: x0 in ].0,d.[ & diff(g,x0) =(g.d-g.0)/(d-0) by A1,A8,A13,A14,FDIFF_1:26,ROLLE:3; ||. diff(f,x0) .|| <= diff(g,x0) by A1,A16,A15; then 0 <= g.d-g.0 by A8,A16; then (0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1 by A12,XREAL_1:7; then (0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1+ e1*d by A8,A2,XREAL_1:7; then ||. f/.d - f/.0 .|| -( (g.d - g.0) + e1+ e1*d ) <= 0 by XREAL_1:47; then ||. f/.d -f/.0 .|| - (g.d - g.0) - e1*d - e1 <= 0; hence d in B by A10; end; then A17: 0 < s by A4,SEQ_4:def 1; now let r be Real; assume r in B; then ex x be Real st r = x & x in [.0,1.] & ||. f/.x -f/.0 .|| - (g.x - g.0 ) - e1*x - e1 <= 0; then ex t be Real st r=t & 0<=t & t<=1; hence r<=1; end; then A18: s <= 1 by A5,SEQ_4:45; defpred P[Nat,Element of REAL] means \$2 in B & |.s-\$2.| <= 1/(\$1+1); A19:now let x be Element of NAT; reconsider t = 1/(1+x) as Real; consider r be Real such that A20: r in B & s-t < r by A4,A5,SEQ_4:def 1; reconsider r as Element of REAL by XREAL_0:def 1; take r; s-t + t < r + t by A20,XREAL_1:8; then A21: s -r < t+r -r by XREAL_1:14; r <= s by A4,A20,SEQ_4:def 1; then 0 <= s - r by XREAL_1:48; hence P[x,r] by A20,A21,SEQ_2:1; end; consider sq be sequence of REAL such that A22: for x being Element of NAT holds P[x, sq.x] from FUNCT_2:sch 3(A19); A23: for x being Nat holds P[x, sq.x] proof let x be Nat; x in NAT by ORDINAL1:def 12; hence thesis by A22; end; reconsider sq as Real_Sequence; A24: now let p1 be Real; assume A25: 0 < p1; set p = p1/2; consider n be Nat such that A26: 1/p < n by SEQ_4:3; 1/p + (0 qua Real) < n+1 by A26,XREAL_1:8; then A27: 1/(n+1) <= 1/(1/p) by A25,XREAL_1:118; take n; thus for m be Nat st n<=m holds |.sq.m-s.| < p1 proof let m be Nat; assume n<=m; then 0 < n+1 & n+1 <= m+1 by XREAL_1:6; then 1/(m+1) <= 1/(n+1) by XREAL_1:118; then A28: 1/(m+1) <= p by A27,XXREAL_0:2; sq.m in B & |.s-sq.m.| <= 1/(m+1) by A23; then |.sq.m-s.| <= 1/(1+m) by COMPLEX1:60; then A29: |.sq.m-s.| <= p by A28,XXREAL_0:2; p < p1 by A25,XREAL_1:216; hence thesis by A29,XXREAL_0:2; end; end; then A30:sq is convergent by SEQ_2:def 6; then A31:lim sq = s by A24,SEQ_2:def 7; deffunc F(Real) = ||. f/.\$1 -f/.0 .|| - (g.\$1 - g.0) - e1*\$1 - e1; A32:for x being Element of REAL holds F(x) in REAL by XREAL_0:def 1; consider Lg0 be Function of REAL,REAL such that A33: for x being Element of REAL holds Lg0.x = F(x) from FUNCT_2:sch 8(A32); A34: for x being Real holds Lg0.x = F(x) proof let x be Real; reconsider x as Element of REAL by XREAL_0:def 1; Lg0.x = F(x) by A33; hence thesis; end; set Lg = Lg0| [.0,1.]; A35: dom Lg0 = REAL by FUNCT_2:def 1; then A36: dom Lg = [.0,1.] by RELAT_1:62; now let y be object; assume y in rng sq; then ex x be object st x in NAT & sq.x = y by FUNCT_2:11; then y in B by A23; then ex x be Real st y=x & x in [.0,1.] & ||. f/.x -f/.0 .|| - (g.x - g.0) - e1*x - e1 <= 0; hence y in [.0,1.]; end; then A37: rng sq c= dom Lg by A36; A38:s in [.0,1.] by A18,A17; now let r be Real; set r3=r/3; assume A39: 0 1; then s < 1 by A18,XXREAL_0:1; then A64: s in ].0,1.[ by A17; then f is_differentiable_in s by A1,NDIFF_3:10; then consider N1 being Neighbourhood of s such that A65: N1 c= dom f & ex L1 be LinearFunc of T,R1 be RestFunc of T st diff(f,s)=L1/.1 & for x be Real st x in N1 holds f/.x-f/.s = L1/.(x-s) + R1/.(x-s) by NDIFF_3:def 4; consider L1 be LinearFunc of T,R1 be RestFunc of T such that A66: diff(f,s)=L1/.1 & for x be Real st x in N1 holds f/.x-f/.s = L1/.(x-s) + R1/.(x-s) by A65; g is_differentiable_in s by A1,A64,FDIFF_1:9; then consider N2 being Neighbourhood of s such that A67: N2 c= dom g & ex L2 be LinearFunc,R2 be RestFunc st diff(g,s)=L2.1 & for x be Real st x in N2 holds g.x-g.s = L2.(x-s) + R2.(x-s) by FDIFF_1:def 5; consider L2 be LinearFunc,R2 be RestFunc such that A68: diff(g,s)=L2.1 & for x be Real st x in N2 holds g.x-g.s = L2.(x-s) + R2.(x-s) by A67; consider NN3 being Neighbourhood of s such that A69: NN3 c= N1 & NN3 c= N2 by RCOMP_1:17; consider g0 be Real such that A70: 0 < g0 & ].s-g0,s+g0.[ c= ].0,1.[ by A64,RCOMP_1:19; reconsider NN4 = ].s-g0,s+g0.[ as Neighbourhood of s by A70,RCOMP_1:def 6; consider N3 being Neighbourhood of s such that A71: N3 c= NN3 & N3 c= NN4 by RCOMP_1:17; consider d1 be Real such that A73: 0 0 & |.t.| < d2 holds ||. (R1/.t) .|| / |.t.| < e2 by A2,Th17; R2 is total & R2 is RestFunc-like by FDIFF_1:def 2; then consider d3 be Real such that A75: 0 0 & |.t.| < d3 holds |.R2.t.|/|.t.| < e2 by A2,Th18; A76: min(d1,d2) <= d1 & min(d1,d2) <= d2 & 0 < min(d1,d2) by A73,A74,XXREAL_0:17,21; set d40= min(min(d1,d2),d3); A77: d40 <= min(d1,d2) & d40 <= d3 & 0 < d40 by A75,A76,XXREAL_0:17,21; set d4=d40/2; A78: d40 <= d1 & d40 <= d2 by A76,A77,XXREAL_0:2; d4 < d40 by A77,XREAL_1:216; then A79a: 0 < d4 & d4 < d1 & d4 < d2 & d4 < d3 by A77,A78,XXREAL_0:2; then s-d1< s+d4 & s+d4< s+d1 by XREAL_1:8; then A80: s+d4 in N3 by A73; then A81: f/.(s+d4)-f/.s = L1/.((s+d4)-s) + R1/.((s+d4)-s) by A66,A71,A69; A82: g.(s+d4)-g.s = L2.((s+d4)-s) + R2.((s+d4)-s) by A71,A69,A80,A68; consider df1 be Point of T such that A83: for p be Real holds L1/.p = p*df1 by NDIFF_3:def 2; L1/.1 = 1*df1 by A83; then L1/.1 = df1 by RLVECT_1:def 8; then A84: L1/.d4 = d4*diff(f,s) by A66,A83; consider df2 be Real such that A85: for p be Real holds L2.p = df2*p by FDIFF_1:def 3; L2.1 = df2*1 by A85; then A86: L2.d4 = d4*diff(g,s) by A68,A85; A87: ||. f/.(s+d4)-f/.s .|| <= ||. L1/.d4 .|| + ||. R1/. d4 .|| by A81,NORMSP_1:def 1; A88: ||. L1/.d4 .|| = |.d4.|*||. diff(f,s) .|| by A84,NORMSP_1:def 1 .= ||. diff(f,s) .||*d4 by A77,ABSVALUE:def 1; A89: 0 < |.d4.| by A77,ABSVALUE:def 1; |.d4.| < d2 by A79a,ABSVALUE:def 1; then ||. R1/.d4 .|| / |.d4.| < e2 by A74,A77; then ||. R1/.d4 .|| <= e2 * |.d4.| by A89,XREAL_1:81; then ||. R1/.d4 .|| <= e2 * d4 by A77,ABSVALUE:def 1; then ||. L1/.d4 .|| + ||. R1/.d4 .|| <= ||. diff(f,s) .|| * d4 + e2 * d4 by A88,XREAL_1:6; then A90: ||. f/.(s+d4)-f/.s .|| <= ||. diff(f,s) .|| * d4 + e2 * d4 by A87,XXREAL_0:2; ||. diff(f,s) .||*d4 <=diff(g,s)*d4 by A64,A1,A77,XREAL_1:64; then ||. diff(f,s) .||*d4 + e2*d4 <= diff(g,s)*d4 + e2*d4 by XREAL_1:6; then A91: ||. f/.(s+d4)-f/.s .|| <= diff(g,s)*d4 + e2*d4 by A90,XXREAL_0:2; |.d4.| < d3 by A79a,ABSVALUE:def 1; then |.R2.d4.|/ |.d4.| < e2 by A75,A77; then |.R2.d4.| <= e2* |.d4.| by A89,XREAL_1:81; then |.R2.d4.| <= e2* d4 by A77,ABSVALUE:def 1; then -(e2*d4) <= R2.d4 by ABSVALUE:5; then d4*diff(g,s) -(e2*d4) <= g.(s+d4)-g.s by A82,A86,XREAL_1:6; then d4*diff(g,s) <= g.(s+d4)-g.s + e2*d4 by XREAL_1:20; then diff(g,s)*d4 + e2*d4 <= (g.(s+d4)-g.s + e2*d4) + e2*d4 by XREAL_1:6; then ||. f/.(s+d4)-f/.s .|| <= g.(s+d4)-g.s + e1*d4 by A91,XXREAL_0:2; then ||. f/.(s+d4)-f/.s .|| - (g.(s+d4)-g.s + e1*d4) <= 0 by XREAL_1:47; then A92: ||. f/.(s+d4)-f/.s .|| - g.(s+d4)+g.s - e1*d4 + (||. f/.s -f/.0 .|| - (g.s - g.0 ) - e1*s - e1) <= (0 qua Real)+ (0 qua Real) by A62; ||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0 + e1*(d4+s) + e1) <= ||. f/.(s+d4)-f/.s .|| + ||. f/.s -f/.0 .|| - (g.(s+d4) -g.0 + e1*(d4+s) + e1) by NORMSP_1:10,XREAL_1:9; then A93: ||. f/.(s+d4)-f/.0 .|| - (g.(s+d4) -g.0) - e1*(s+d4) -e1 <= 0 by A92; |.(0 qua Real)+1-2*(s+d4).|< 1 -(0 qua Real) by A80,A71,A70,RCOMP_1:3; then s + d4 in [.0,1.] by RCOMP_1:2; then A94: s+d4 in B by A93; s +(0 qua Real) < s + d4 by A77,XREAL_1:8; hence contradiction by A94,A4,SEQ_4:def 1; end; 0 in dom g & 1 in dom g by A1; then g/.1 = g.1 & g/.0 = g.0 by PARTFUN1:def 6; then ||. f/.1 -f/.0 .|| - (g/.1 - g/.0 ) - e + e <= (0 qua Real) + e by A63,A62,XREAL_1:6; hence ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) <= e; end; then ||. f/.1 -f/.0 .|| - (g/.1 - g/.0) + (g/.1 - g/.0) <= (0 qua Real) + (g/.1 - g/.0) by Lm3,XREAL_1:6; hence thesis; end; theorem Th19: for S,T be RealNormSpace, f be PartFunc of S,T, p,q be Point of S, M be Real st [.p,q.] c= dom f & (for x be Point of S st x in [.p,q.] holds f is_continuous_in x) & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x) & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M) holds ||. f/.q - f/.p .|| <= M*||. q-p .|| proof let S,T be RealNormSpace, f be PartFunc of S,T, p,q be Point of S, M be Real; assume A1: [.p,q.] c= dom f & (for x be Point of S st x in [.p,q.] holds f is_continuous_in x) & (for x be Point of S st x in ].p,q.[ holds f is_differentiable_in x) & (for x be Point of S st x in ].p,q.[ holds ||. diff(f,x) .|| <= M); per cases ; suppose B2: p=q ; B3: ||. f/.q - f/.p .|| = ||. 0.T .|| by B2,RLVECT_1:15 .= 0; M*||. q-p .|| = M * ||. 0.S .|| by B2,RLVECT_1:15 .= 0 ; hence thesis by B3; end; suppose p<>q ; then X1: ]. p,q .[ = { p+t*(q-p) where t is Real : 0 < t & t < 1} by LMOPN; deffunc PP(Real) = \$1*(q-p)+p; consider pt0 be Function of REAL,the carrier of S such that A2: for t being Element of REAL holds pt0.t = PP(t) from FUNCT_2:sch 4; A3: for t being Real holds pt0.t = PP(t) proof let t be Real; reconsider t as Element of REAL by XREAL_0:def 1; pt0.t = PP(t) by A2; hence thesis; end; set pt=pt0 | ([.0,1.]); A4:dom pt0 = REAL by FUNCT_2:def 1; then A5:dom pt = [.0,1.] by RELAT_1:62; A6:now let t be Real; assume t in [.0,1.]; pt0/.t = pt0.t by A4,PARTFUN1:def 6,XREAL_0:def 1; hence pt0/.t = t*(q-p)+p by A3; end; A7: ].0,1.[ c= [.0,1.] by XXREAL_1:25; A8:now let t be Real; assume t in ].0,1.[; hence pt/.t = pt0/.t by A5,A7,PARTFUN2:15 .= pt0.t by A4,PARTFUN1:def 6,XREAL_0:def 1 .= t*(q-p)+p by A3; end; then A10:pt is_differentiable_on ].0,1.[ & for t be Real st t in ].0,1.[ holds (pt`|].0,1.[ ).t = (q-p) by A5,A7,NDIFF_3:21; reconsider phi = f*pt as PartFunc of REAL,T; A11:rng pt c= [.p,q.] proof let y be object; assume y in rng pt; then consider x be object such that A12: x in dom pt & y = pt.x by FUNCT_1:def 3; A13: y = pt0.x by A12,FUNCT_1:47; reconsider x as Element of REAL by A12; consider r be Real such that A14: x=r & 0<=r & r<=1 by A12,A5; y = p+ x*(q-p) by A3,A13 .= (1-x)*p + x*q by Lm2; then y in {(1-r1)*p + r1*q where r1 is Real : 0 <= r1 & r1 <= 1 } by A14; hence y in [. p,q .] by RLTOPSP1:def 2; end; then rng pt c= dom f by A1; then A15: dom phi = [.0,1.] by A5,RELAT_1:27; A16: for t be Real st t in [.0,1.] holds phi/.t = f/.(p+t*(q-p)) proof let t be Real; assume A17: t in [.0,1.]; then A18: phi/.t =phi.t by A15,PARTFUN1:def 6 .= f.(pt.t) by A17,A15,FUNCT_1:12; A19: pt.t in rng pt by A17,A5,FUNCT_1:def 3; pt.t = pt0.t by A17,A5,FUNCT_1:47 .= p+t*(q-p) by A3; hence thesis by A18,A11,A19,A1,PARTFUN1:def 6; end; now let x0 be Real; assume A20: x0 in dom phi; then A21: pt is_continuous_in x0 by A5,A6,A15,NFCONT_3:33,def 2; pt.x0 in rng pt by A5,A20,A15,FUNCT_1:def 3; then pt.x0 in [.p,q.] by A11; then pt/.x0 in [.p,q.] by A20,A15,A5,PARTFUN1:def 6; hence phi is_continuous_in x0 by A1,A20,A21,NFCONT_3:15; end; then phi is continuous by NFCONT_3:def 2; then A22:phi| [.0,1.] is continuous; A23: now let x be Real; assume A24: x in ].0,1.[; then A25: pt is_differentiable_in x by A10,NDIFF_3:10; (pt`|].0,1.[ ).x = (q-p) by A24,A8,A5,A7,NDIFF_3:21; then A26: diff(pt,x) = (q-p) by A10,A24,NDIFF_3:def 6; A27: pt.x = pt/.x by A24,A7,A5,PARTFUN1:def 6; A28: ex r be Real st x=r & 0 0.T as PartFunc of S,T; A7:dom R = the carrier of S by FUNCOP_1:13; now let h be (0.S)-convergent sequence of S; assume h is non-zero; A8: now let n be Nat; A9: R/.(h.n) =R.(h.n) by A7,PARTFUN1:def 6 .=0.T by FUNCOP_1:7; A10: rng h c= dom R by A7; A11: n in NAT by ORDINAL1:def 12; thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by NDIFF_1:def 2 .=(||.h.||".n)*(R/.(h.n)) by A11,A10,FUNCT_2:109 .=0.T by A9,RLVECT_1:10; end; then A12: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18; hence (||.h.||")(#)(R/*h) is convergent by NDIFF_1:18; ((||.h.||")(#)(R/*h)).0 = 0.T by A8; hence lim ((||.h.||")(#)(R/*h)) = 0.T by A12,NDIFF_1:18; end; then reconsider R as RestFunc of S,T by NDIFF_1:def 5; A13: now let x0 be Point of S; set N = the Neighbourhood of x0; A14:for x be Point of S st x in N holds L0/.x-L0/.x0=L.(x-x0)+R/.(x-x0) proof let x be Point of S; A15: R/.(x-x0) =R.(x-x0) by A7,PARTFUN1:def 6 .=0.T by FUNCOP_1:7; assume x in N; thus L0/.x-L0/.x0 = L.(x-p)-L0/.x0 by A3 .= L.(x-p)-L.(x0-p) by A3 .= LP.(x-p)+(-1)*LP.(x0-p) by RLVECT_1:16 .= LP.(x-p)+LP.((-1)*(x0-p)) by LOPBAN_1:def 5 .= LP.((x-p)+(-1)*(x0-p)) by VECTSP_1:def 20 .= LP.((x-p)-(x0-p)) by RLVECT_1:16 .= LP.(x-((x0-p)+p)) by RLVECT_1:27 .= LP.(x-(x0-(p-p))) by RLVECT_1:29 .= LP.(x-(x0-0.S)) by RLVECT_1:15 .= LP.(x-x0) by RLVECT_1:13 .= L.(x-x0) + R/.(x-x0) by A15,RLVECT_1:4; end; hence L0 is_differentiable_in x0 by A4,NDIFF_1:def 6; hence diff(L0,x0) = L by A4,A14,NDIFF_1:def 7; end; set g= f - L0; A16:dom g = dom f /\ dom L0 by VFUNCT_1:def 2 .= dom f by A4,XBOOLE_1:28; A17:for x be Point of S st x in dom g holds g/.x= f/.x - L.(x-p) proof let x be Point of S; assume x in dom g; hence g/.x= f/.x - L0/.x by VFUNCT_1:def 2 .=f/.x - L.(x-p) by A3; end; A18:for x be Point of S st x in [.p,q.] holds g is_continuous_in x proof let x be Point of S; assume x in [.p,q.]; then A19:f is_continuous_in x by A2; L0 | (dom L0) is_continuous_in x by A4,A6,NFCONT_1:def 7; hence thesis by A19,NFCONT_1:15; end; A20:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x proof let x be Point of S; assume x in ].p,q.[; then f is_differentiable_in x & L0 is_differentiable_in x by A2,A13; hence g is_differentiable_in x by NDIFF_1:36; end; for x be Point of S st x in ].p,q.[ holds ||. diff(g,x) .|| <= M proof let x be Point of S; assume A21: x in ].p,q.[; then A22: f is_differentiable_in x by A2; L0 is_differentiable_in x & diff(L0,x) = L by A13; then diff(g,x) = diff(f,x) - L by A22,NDIFF_1:36; hence ||. diff(g,x) .|| <= M by A2,A21; end; then A23: ||. g/.q - g/.p .|| <= M*||. q-p .|| by Th19,A1,A16,A18,A20; p in [.p,q.] by RLTOPSP1:68; then g/.p= f/.p - L.(p-p) by A1,A16,A17; then A24:g/.p = f/.p - LP.(0.S) by RLVECT_1:15 .=f/.p - LP.( 0 *p ) by RLVECT_1:10 .=f/.p - 0 * LP.p by LOPBAN_1:def 5 .=f/.p - 0.T by RLVECT_1:10 .=f/.p by RLVECT_1:13; q in [.p,q.] by RLTOPSP1:68; then g/.q= f/.q - L.(q-p) by A1,A16,A17; then f/.q - (L.(q-p) +f/.p ) = g/.q - g/.p by A24,RLVECT_1:27; hence thesis by A23,RLVECT_1:27; end; begin :: Partial derivative of a function of several variables definition let G be RealNormSpace-Sequence; let i be Element of dom G; func proj i -> Function of product G,G.i means :Def3: for x be Element of product carr G holds it.x = x.i; existence proof deffunc F(Element of product carr G) = \$1.i; consider f being Function of product carr G,G.i such that A1: for x being Element of product carr G holds f.x = F(x) from FUNCT_2:sch 4; product G = NORMSTR(# product carr G,zeros G,[:addop G:] ,[:multop G:], productnorm G #) by PRVECT_2:6; then reconsider f as Function of product G,G.i; take f; thus thesis by A1; end; uniqueness proof let f,g be Function of the carrier of (product G),the carrier of (G.i); assume that A2: for x being Element of product carr G holds f.x = x.i and A3: for x being Element of product carr G holds g.x = x.i; A4:product G = NORMSTR(# product carr G,zeros G,[:addop G:] ,[:multop G:], productnorm G #) by PRVECT_2:6; now let x1 be Element of the carrier of product G; reconsider x=x1 as Element of product carr G by A4; f.x1 =x.i by A2; hence f.x1 = g.x1 by A3; end; hence thesis; end; end; definition let G be RealNormSpace-Sequence; let i be Element of dom G; let x be Element of product G; func reproj(i,x) -> Function of G.i,product G means :Def4: for r be Element of G.i holds it.r = x +* (i,r); existence proof reconsider x1 = x as Element of product carr G by Th10; defpred P[Element of G.i, Element of the carrier of product G] means \$2 = x1 +* (i,\$1); A1:for r being Element of G.i ex y be Element of the carrier of product G st P[r,y] proof let r be Element of G.i; x1 +* (i,r) is Element of the carrier of product G by Th11; hence thesis; end; ex f being Function of the carrier of (G.i),the carrier of product G st for r be Element of G.i holds P[r,f.r] from FUNCT_2:sch 3(A1); hence thesis; end; uniqueness proof let f,g be Function of the carrier of (G.i),the carrier of product G; assume that A2:for r be Element of G.i holds f.r = x +* (i,r) and A3:for r be Element of G.i holds g.r = x +* (i,r); let r be Element of G.i; f.r = x +* (i,r) by A2; hence f.r = g.r by A3; end; end; definition ::\$CD let G be RealNormSpace-Sequence; let F be RealNormSpace; let i be set; let f be PartFunc of product G,F; let x being Element of product G; pred f is_partial_differentiable_in x,i means f*reproj(In(i,dom G),x) is_differentiable_in proj(In(i,dom G)).x; end; definition let G be RealNormSpace-Sequence; let F be RealNormSpace; let i be set; let f be PartFunc of product G,F; let x be Point of product G; func partdiff(f,x,i) -> Point of R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),F) equals diff(f*reproj(In(i,dom G),x),proj(In(i,dom G)).x); coherence; end; begin :: Linearity of Partial Differential Operator reserve G for RealNormSpace-Sequence; reserve F for RealNormSpace; reserve i for Element of dom G; reserve f,f1,f2 for PartFunc of product G, F; reserve x for Point of product G; reserve X for set; definition let G be RealNormSpace-Sequence; let F be RealNormSpace; let i be set; let f be PartFunc of product G,F; let X be set; pred f is_partial_differentiable_on X,i means X c= dom f & for x be Point of product G st x in X holds f|X is_partial_differentiable_in x,i; end; theorem Th21: for xi be Element of G.i holds ||. reproj(i,0.(product G)).xi .|| = ||.xi.|| proof let xi be Element of G.i; set j = len G; reconsider i0 = i as Element of NAT; Seg len G = dom G by FINSEQ_1:def 3; then A1:1 <= i0 & i0 <= j by FINSEQ_1:1; set z = 0.(product G); A3: the carrier of (product G) = product carr G by Th10; then reconsider w = z +* (i0,xi) as Element of product carr G by Th11; A4: ||. reproj(i,z).xi .|| = |. normsequence(G,w) .| by Def4,PRVECT_2:7; reconsider q = ||.xi.|| as Element of REAL; set q1 = <*q*>; set y = 0*j; A5:len normsequence(G,w) = j by PRVECT_2:def 11; A6:len y = j by CARD_1:def 7; then A7:(y| (i0-'1))^<*q*>^(y /^ i0) = Replace(y,i0,q) by A1,FINSEQ_7:def 1; then A8:len ((y| (i0-'1))^<*q*>^(y /^ i0)) = len y by FINSEQ_7:5; A9:len y = len Replace(y,i0,q) by FINSEQ_7:5; for k be Nat st 1 <= k & k <= len normsequence(G,w) holds normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k proof let k be Nat; assume A10: 1 <= k & k <= len normsequence(G,w); then reconsider k1 = k as Element of dom G by A5,FINSEQ_3:25; A11: k1 in dom G; z in the carrier of product G; then z in product carr G by Th10; then consider g being Function such that A12: z = g & dom g = dom carr G & for y being object st y in dom carr G holds g.y in (carr G).y by CARD_3:def 5; A13: k in dom z by A11,A12,Lm1; A14: (normsequence(G,w)).k = (the normF of (G.k1)).(w.k1) by PRVECT_2:def 11; per cases; suppose A15: k = i0; then A16: (normsequence(G,w)).k = ||. xi .|| by A14,A13,FUNCT_7:31; Replace(y,i0,q)/.k = q by A15,A10,A5,A6,FINSEQ_7:8; hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k by A16,A7,A10,A5,A6,A9,FINSEQ_4:15; end; suppose A17: k <> i0; then w.k1 = z.k1 by FUNCT_7:32; then A18: (normsequence(G,w)).k = ||. 0.(G.k1) .|| by A14,Th14,A3; Replace(y,i0,q)/.k = y/.k by A17,A10,A5,A6,FINSEQ_7:10; then Replace(y,i0,q).k = y/.k by A10,A5,A6,A9,FINSEQ_4:15; then Replace(y,i0,q).k = y.k by A10,A5,A6,FINSEQ_4:15; hence normsequence(G,w).k = ((y| (i0-'1))^<*q*>^(y /^ i0)).k by A18,A6,A1,FINSEQ_7:def 1; end; end; then A19:normsequence(G,w) = (y| (i0-'1))^<*q*>^(y /^ i0) by A6,A8,PRVECT_2:def 11; sqrt Sum sqr(y| (i0-'1)) = |. 0*(i0-'1) .| by A1,PDIFF_7:2; then sqrt Sum sqr(y| (i0-'1)) = 0 by EUCLID:7; then A20:Sum sqr(y| (i0-'1)) = 0 by RVSUM_1:86,SQUARE_1:24; sqrt Sum sqr(y/^i0) = |. 0*(j-'i0) .| by PDIFF_7:3; then A21:sqrt Sum sqr(y/^i0) = 0 by EUCLID:7; reconsider q2 = q^2 as Element of REAL by XREAL_0:def 1; sqr((y| (i0-'1))^<*q*>^(y/^i0)) = sqr((y| (i0-'1))^<*q*>)^sqr(y/^i0) by RVSUM_1:144 .= sqr(y| (i0-'1))^sqr<*q*>^sqr(y/^i0) by RVSUM_1:144 .= sqr(y| (i0-'1))^<*q^2*>^sqr(y/^i0) by RVSUM_1:55; then Sum sqr((y| (i0-'1))^<*q*>^(y/^i0)) = Sum(sqr(y| (i0-'1))^<*q2*>) + Sum sqr(y/^i0) by RVSUM_1:75 .= Sum sqr(y| (i0-'1)) + q^2 + Sum sqr(y/^i0) by RVSUM_1:74 .= q^2 by A20,A21,RVSUM_1:86,SQUARE_1:24; then ||. reproj(i,z).xi .|| = |. q .| by A19,A4,COMPLEX1:72; hence thesis by COMPLEX1:43; end; theorem Th22: for G be RealNormSpace-Sequence, i be Element of dom G, x be Point of product G, r be Point of G.i holds reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x) & x - reproj(i,x).r = reproj(i,0.(product G)).(proj(i).x - r) proof let G be RealNormSpace-Sequence, i be Element of dom G, x be Point of product G, r be Point of G.i; set m=len G; reconsider xf=x as Element of product carr G by Th10; A1:dom carr G = dom G by Lm1; reconsider Zr = 0.(product G) as Element of product carr G by Th10; reconsider ixr = reproj(i,x).r as Element of product carr G by Th10; reconsider p = reproj(i,x).r - x as Element of product carr G by Th10; reconsider q = reproj(i,0.(product G)).(r - proj(i).x) as Element of product carr G by Th10; A3:dom q = dom (carr G) by CARD_3:9; reconsider s = x - reproj(i,x).r as Element of product carr G by Th10; reconsider t = reproj(i,0.(product G)).(proj(i).x - r) as Element of product carr G by Th10; A5:dom t = dom carr G by CARD_3:9; A6: reproj(i,x).r = x +* (i,r) by Def4; reconsider xfi =xf.i as Point of G.i; A7: reproj(i,0.(product G)).(r - proj(i).x) = 0.(product G) +* (i,(r - proj(i).x)) by Def4; then A7a: q = Zr +* (i,(r- xfi)) by Def3; A8: reproj(i,0.(product G)).(proj(i).x -r) = 0.(product G) +* (i,(proj(i).x - r)) by Def4; then A8a: t = Zr +* (i,(xfi -r)) by Def3; set ir= i .--> r; set irx1= (i .--> (r- xfi)); set irx2= (i .--> (xfi - r)); x in the carrier of product G; then A9: x in product carr G by Th10; consider g1 be Function such that A10: x = g1 & dom g1 = dom carr G & for i be object st i in dom carr G holds g1.i in (carr G).i by A9,CARD_3:def 5; for k be object st k in dom p holds p.k = q.k proof let k be object; assume A11: k in dom p; then reconsider k0=k as Element of dom G by A1,CARD_3:9; consider g be Function such that A12: Zr = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A13: k in dom Zr by A12,A11,CARD_3:9; A14: k in dom x by A10,A11,CARD_3:9; per cases; suppose not k in {i}; then A15: k <> i by TARSKI:def 1; then A16: q.k0 = Zr.k0 by A7,FUNCT_7:32; p.k = ixr.k0 -xf.k0 by Th15 .= xf.k0 -xf.k0 by A15,A6,FUNCT_7:32; then p.k =0.(G.k0) by RLVECT_1:15; hence p.k = q.k by A16,Th14; end; suppose k in {i}; then A17: k=i by TARSKI:def 1; then A18: q.k0 = r- xfi by A7a,A13,FUNCT_7:31; p.k=ixr.k0 -xf.k0 by Th15; hence p.k = q.k by A18,A6,A17,A14,FUNCT_7:31; end; end; hence reproj(i,x).r - x = reproj(i,0.(product G)).(r - proj(i).x) by A3,FUNCT_1:2,CARD_3:9; for k be object st k in dom s holds s.k = t.k proof let k be object; assume A19: k in dom s; then reconsider k0=k as Element of dom G by A1,CARD_3:9; consider g be Function such that A20: Zr = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A21: k in dom Zr by A20,A19,CARD_3:9; A22: k in dom x by A10,A19,CARD_3:9; per cases; suppose not k in {i}; then A23: k <> i by TARSKI:def 1; then A24: t.k0 = Zr.k0 by A8,FUNCT_7:32; s.k= xf.k0 - ixr.k0 by Th15 .=xf.k0 -xf.k0 by A6,A23,FUNCT_7:32; then s.k =0.(G.k0) by RLVECT_1:15; hence s.k = t.k by A24,Th14; end; suppose k in {i}; then A25: k=i by TARSKI:def 1; then A26: t.k0 = xfi-r by A8a,A21,FUNCT_7:31; s.k=xf.k0 - ixr.k0 by Th15; hence s.k = t.k by A26,A6,A25,A22,FUNCT_7:31; end; end; hence thesis by A5,FUNCT_1:2,CARD_3:9; end; theorem Th23: for G be RealNormSpace-Sequence, i be Element of dom G, x be Point of product G, Z be Subset of product G st Z is open & x in Z holds ex N be Neighbourhood of proj(i).x st for z be Point of G.i st z in N holds (reproj(i,x)).z in Z proof let G be RealNormSpace-Sequence, i be Element of dom G, x be Point of product G, Z be Subset of product G; assume Z is open & x in Z; then consider r be Real such that A1: 0 < r & {y where y is Point of product G : ||. y - x .|| < r} c= Z by NDIFF_1:3; set N = {y where y is Point of G.i : ||. y - proj(i).x .|| < r}; reconsider N as Neighbourhood of proj(i).x by A1,NFCONT_1:3; take N; thus for z be Point of G.i st z in N holds (reproj(i,x)).z in Z proof let z be Point of G.i; assume z in N; then A2: ex y be Point of G.i st y = z & ||. y - proj(i).x .|| < r; ||. (reproj(i,x)).z - x .|| = ||. reproj(i,0.(product G)).(z - proj(i).x) .|| by Th22 .= ||. z - proj(i).x .|| by Th21; then (reproj(i,x)).z in {y where y is Point of product G : ||. y - x .|| < r} by A2; hence thesis by A1; end; end; theorem Th24: for G be RealNormSpace-Sequence, T be RealNormSpace, i be set, f be PartFunc of product G, T, Z be Subset of product G st Z is open holds f is_partial_differentiable_on Z,i iff Z c=dom f & for x be Point of product G st x in Z holds f is_partial_differentiable_in x,i proof let G be RealNormSpace-Sequence, T be RealNormSpace, i be set, f be PartFunc of product G, T, Z be Subset of product G; assume A1: Z is open; set i0=In(i,dom G); set S=G.i0; set RNS= R_NormSpace_of_BoundedLinearOperators(S,T); thus f is_partial_differentiable_on Z,i implies Z c=dom f & for x be Point of product G st x in Z holds f is_partial_differentiable_in x,i proof assume A2: f is_partial_differentiable_on Z,i; hence Z c=dom f; let nx0 be Point of product G; reconsider x0=proj(i0).nx0 as Point of S; assume A4: nx0 in Z; then f|Z is_partial_differentiable_in nx0,i by A2; then consider N0 being Neighbourhood of x0 such that A5: N0 c= dom((f|Z)*reproj(i0,nx0)) and A6: ex L be Point of RNS,R be RestFunc of S,T st for x be Point of S st x in N0 holds ((f|Z)*reproj(i0,nx0))/.x-((f|Z)*reproj(i0,nx0))/.x0 = L .( x-x0)+R/.(x-x0) by NDIFF_1:def 6; consider L be Point of RNS,R be RestFunc of S,T such that A7: for x be Point of S st x in N0 holds ((f|Z)*reproj(i0,nx0))/.x - ((f|Z)*reproj(i0,nx0))/.x0 = L.(x-x0) + R/.(x-x0) by A6; consider N1 being Neighbourhood of x0 such that A8: for x be Point of S st x in N1 holds (reproj(i0,nx0)).x in Z by A1,A4,Th23; A9:now let x be Point of S; assume x in N1; then (reproj(i0,nx0)).x in Z by A8; then (reproj(i0,nx0)).x in (dom f) /\ Z by A2,XBOOLE_0:def 4; hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61; end; reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8; (f|Z)*reproj(i0,nx0) c= f*reproj(i0,nx0) by RELAT_1:29,59; then A10:dom((f|Z)*reproj(i0,nx0)) c= dom(f*reproj(i0,nx0)) by RELAT_1:11; N c= N0 by XBOOLE_1:17; then A11:N c= dom(f*reproj(i0,nx0)) by A5,A10; now let x be Point of S; assume A12: x in N; then A13: x in N0 by XBOOLE_0:def 4; A14: dom(reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1; x in N1 by A12,XBOOLE_0:def 4; then A15: (reproj(i0,nx0)).x in dom(f|Z) by A9; then A16: (reproj(i0,nx0)).x in dom f & (reproj(i0,nx0)).x in Z by RELAT_1:57; A17: (reproj(i0,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then A18: (reproj(i0,nx0)).x0 in dom f & (reproj(i0,nx0)).x0 in Z by RELAT_1:57; A19: ((f|Z)*reproj(i0,nx0))/.x =(f|Z)/.(reproj(i0,nx0)/.x) by A15,A14,PARTFUN2:4 .= f/. (reproj(i0,nx0)/.x) by A16,PARTFUN2:17 .= (f*reproj(i0,nx0))/.x by A14,A16,PARTFUN2:4; ((f|Z)*reproj(i0,nx0))/.x0 =(f|Z)/. (reproj(i0,nx0)/.x0 ) by A14,A17,PARTFUN2:4 .= f/. (reproj(i0,nx0)/.x0) by A18,PARTFUN2:17 .= (f*reproj(i0,nx0))/.x0 by A14,A18,PARTFUN2:4; hence (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0 =L.(x-x0)+R/.(x-x0) by A7,A13,A19; end; hence f is_partial_differentiable_in nx0,i by A11,NDIFF_1:def 6; end; assume that A20:Z c=dom f and A21:for nx be Point of product G st nx in Z holds f is_partial_differentiable_in nx,i; now let nx0 be Point of product G; assume A22: nx0 in Z; then A23:f is_partial_differentiable_in nx0,i by A21; reconsider x0=proj(i0).nx0 as Point of S; consider N0 being Neighbourhood of x0 such that N0 c= dom (f*reproj(i0,nx0)) and A24: ex L be Point of RNS,R be RestFunc of S,T st for x be Point of S st x in N0 holds (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0 = L.(x-x0)+R /.(x-x0) by A23,NDIFF_1:def 6; consider N1 being Neighbourhood of x0 such that A25: for x be Point of S st x in N1 holds (reproj(i0,nx0)).x in Z by A1,A22,Th23; A26:now let x be Point of S; assume x in N1; then (reproj(i0,nx0)).x in Z by A25; then (reproj(i0,nx0)).x in (dom f) /\ Z by A20,XBOOLE_0:def 4; hence (reproj(i0,nx0)).x in dom(f|Z) by RELAT_1:61; end; A27:N1 c= dom((f|Z)*reproj(i0,nx0)) proof let z be object; assume A28:z in N1; then A29: z in the carrier of S; reconsider x=z as Point of S by A28; A30: (reproj(i0,nx0)).x in dom(f|Z) by A28,A26; z in dom (reproj(i0,nx0)) by A29,FUNCT_2:def 1; hence z in dom((f|Z)*reproj(i0,nx0)) by A30,FUNCT_1:11; end; reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8; N c= N1 by XBOOLE_1:17; then A31:N c= dom((f|Z)*reproj(i0,nx0)) by A27; consider L be Point of RNS,R be RestFunc of S,T such that A32: for x be Point of S st x in N0 holds (f*reproj(i0,nx0))/.x-(f*reproj(i0,nx0))/.x0=L.(x-x0)+R/.(x-x0) by A24; now let x be Point of S; assume A33: x in N; then A34: x in N0 by XBOOLE_0:def 4; A35: dom (reproj(i0,nx0)) = the carrier of G.i0 by FUNCT_2:def 1; x in N1 by A33,XBOOLE_0:def 4; then A36: (reproj(i0,nx0)).x in dom(f|Z) by A26; then A37: (reproj(i0,nx0)).x in dom f /\ Z by RELAT_1:61; then A38: (reproj(i0,nx0)).x in dom f by XBOOLE_0:def 4; A39: (reproj(i0,nx0)).x0 in dom(f|Z) by A26,NFCONT_1:4; then A40: (reproj(i0,nx0)).x0 in dom f /\ Z by RELAT_1:61; then A41: (reproj(i0,nx0)).x0 in dom f by XBOOLE_0:def 4; A42: ((f|Z)*reproj(i0,nx0))/.x = (f|Z)/.(reproj(i0,nx0)/.x) by A36,A35,PARTFUN2:4 .= f/.(reproj(i0,nx0)/.x) by A37,PARTFUN2:16 .= (f*reproj(i0,nx0))/.x by A35,A38,PARTFUN2:4; ((f|Z)*reproj(i0,nx0))/.x0 = (f|Z)/. (reproj(i0,nx0)/.x0 ) by A35,A39,PARTFUN2:4 .= f/. (reproj(i0,nx0)/.x0) by A40,PARTFUN2:16 .= (f*reproj(i0,nx0))/.x0 by A35,A41,PARTFUN2:4; hence ((f|Z)*reproj(i0,nx0))/.x -((f|Z)*reproj(i0,nx0))/.x0 = L.(x-x0)+R/.(x-x0) by A42,A34,A32; end; hence (f|Z) is_partial_differentiable_in nx0,i by A31,NDIFF_1:def 6; end; hence thesis by A20; end; theorem for i be set st i in dom G & f is_partial_differentiable_on X,i holds X is Subset of product G by XBOOLE_1:1; definition let G be RealNormSpace-Sequence; let S be RealNormSpace; let i be set; let f be PartFunc of product G, S; let X be set; assume A2: f is_partial_differentiable_on X,i; func f `partial|(X,i) -> PartFunc of product G, R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S) means :Def9: dom it = X & for x be Point of product G st x in X holds it/.x = partdiff(f,x,i); existence proof deffunc F(Element of product G) = partdiff(f,\$1,i); defpred P[Element of product G] means \$1 in X; consider F being PartFunc of product G, R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S) such that A3: (for x be Point of product G holds x in dom F iff P[x]) & for x be Point of product G st x in dom F holds F.x = F(x) from SEQ_1:sch 3; take F; now A4: X is Subset of product G by A2,XBOOLE_1:1; let y be object; assume y in X; hence y in dom F by A3,A4; end; then A5:X c= dom F; dom F c= X by A3; hence dom F = X by A5,XBOOLE_0:def 10; hereby let x be Point of product G; assume A6: x in X; then F.x = partdiff(f,x,i) by A3; hence F/.x = partdiff(f,x,i) by A3,A6,PARTFUN1:def 6; end; end; uniqueness proof let F,H be PartFunc of product G, R_NormSpace_of_BoundedLinearOperators(G.In(i,dom G),S); assume that A7: dom F = X and A8: for x be Point of product G st x in X holds F/.x = partdiff(f,x,i) and A9: dom H = X and A10: for x be Point of product G st x in X holds H/.x = partdiff(f,x,i); now let x be Point of product G; assume A11: x in dom F; then F/.x = partdiff(f,x,i) by A7,A8; hence F/.x=H/.x by A7,A10,A11; end; hence thesis by A7,A9,PARTFUN2:1; end; end; theorem Th26: for i be set st i in dom G holds (f1+f2)*reproj(In(i,dom G),x) = f1*reproj(In(i,dom G),x) +f2*reproj(In(i,dom G),x) & (f1-f2)*reproj(In(i,dom G),x) = f1*reproj(In(i,dom G),x) -f2*reproj(In(i,dom G),x) proof let i0 be set; assume i0 in dom G; set i=In(i0,dom G); A1:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1; A2:dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1; A3b: for s be Element of G.i holds s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)+f2*reproj(i,x)) proof let s be Element of G.i; s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2 by A2,A1,FUNCT_1:11; then s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2 by XBOOLE_0:def 4; then s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x)) by A1,FUNCT_1:11; then s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4; hence thesis by VFUNCT_1:def 1; end; then A3:for s be object holds s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x) + f2*reproj(i,x)); then A3a:dom((f1+f2)*reproj(i,x)) = dom(f1*reproj(i,x)+f2*reproj(i,x)) by TARSKI:2; A4:for z being Element of G.i st z in dom((f1+f2)*reproj(i,x)) holds ((f1+f2)*reproj(i,x)).z = (f1*reproj(i,x)+f2*reproj(i,x)).z proof let z be Element of G.i; assume A5: z in dom((f1+f2)*reproj(i,x)); then A6: reproj(i,x).z in dom(f1+f2) by FUNCT_1:11; z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by A3a,A5,VFUNCT_1:def 1; then A7: z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4; A8: reproj(i,x).z in dom f1 /\ dom f2 by A2,A5,FUNCT_1:11; then reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then A9:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6 .=(f1*reproj(i,x)).z by A7,FUNCT_1:12 .=(f1*reproj(i,x))/.z by A7,PARTFUN1:def 6; reproj(i,x).z in dom f2 by A8,XBOOLE_0:def 4; then A10:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6 .=(f2*reproj(i,x)).z by A7,FUNCT_1:12 .=(f2*reproj(i,x))/.z by A7,PARTFUN1:def 6; ((f1+f2)*reproj(i,x)).z = (f1+f2).(reproj(i,x).z) by A5,FUNCT_1:12 .=(f1+f2)/.(reproj(i,x).z) by A6,PARTFUN1:def 6 .= f1/.(reproj(i,x).z) +f2/.(reproj(i,x).z) by A6,VFUNCT_1:def 1 .=(f1*reproj(i,x)+ f2*reproj(i,x))/.z by A3b,A5,A9,A10,VFUNCT_1:def 1; hence thesis by A3b,A5,PARTFUN1:def 6; end; A11: dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2; A12b: for s be Element of G.i holds s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)-f2*reproj(i,x)) proof let s be Element of G.i; s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2 by A11,A1,FUNCT_1:11; then s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 & reproj(i,x).s in dom f2 by XBOOLE_0:def 4; then s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) & s in dom(f2*reproj(i,x)) by A1,FUNCT_1:11; then s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by XBOOLE_0:def 4; hence thesis by VFUNCT_1:def 2; end; then A12: for s be object holds s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x) - f2*reproj(i,x)); then A12a: dom((f1-f2)*reproj(i,x)) = dom(f1*reproj(i,x)-f2*reproj(i,x)) by TARSKI:2; for z being Element of G.i st z in dom((f1-f2)*reproj(i,x)) holds ((f1-f2)*reproj(i,x)).z = (f1*reproj(i,x)-f2*reproj(i,x)).z proof let z be Element of G.i; assume A13: z in dom((f1-f2)*reproj(i,x)); then A14:reproj(i,x).z in dom (f1-f2) by FUNCT_1:11; z in dom(f1*reproj(i,x)) /\ dom(f2*reproj(i,x)) by A12a,A13,VFUNCT_1:def 2; then A15:z in dom(f1*reproj(i,x)) & z in dom(f2*reproj(i,x)) by XBOOLE_0:def 4; A16:reproj(i,x).z in dom f1 /\ dom f2 by A11,A13,FUNCT_1:11; then reproj(i,x).z in dom f1 by XBOOLE_0:def 4; then A17:f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by PARTFUN1:def 6 .=(f1*reproj(i,x)).z by A15,FUNCT_1:12 .=(f1*reproj(i,x))/.z by A15,PARTFUN1:def 6; reproj(i,x).z in dom f2 by A16,XBOOLE_0:def 4; then A18:f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by PARTFUN1:def 6 .=(f2*reproj(i,x)).z by A15,FUNCT_1:12 .=(f2*reproj(i,x))/.z by A15,PARTFUN1:def 6; thus ((f1-f2)*reproj(i,x)).z =(f1-f2).(reproj(i,x).z) by A13,FUNCT_1:12 .=(f1-f2)/.(reproj(i,x).z) by A14,PARTFUN1:def 6 .= f1/.(reproj(i,x).z) - f2/.(reproj(i,x).z) by A14,VFUNCT_1:def 2 .=(f1*reproj(i,x)- f2*reproj(i,x))/.z by A12b,A13,A17,A18,VFUNCT_1:def 2 .=(f1*reproj(i,x)- f2*reproj(i,x)).z by A12b,A13,PARTFUN1:def 6; end; hence thesis by A3,A12,A4,TARSKI:2,PARTFUN1:5; end; theorem Th27: for i be set st i in dom G holds r(#)(f*reproj(In(i,dom G),x)) = (r(#)f)*reproj(In(i,dom G),x) proof let i0 be set; assume i0 in dom G; set i=In(i0,dom G); A1:dom(r(#)f) = dom f by VFUNCT_1:def 4; A2:dom(r(#)(f*reproj(i,x))) =dom(f*reproj(i,x)) by VFUNCT_1:def 4; A3:dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1; A4b: for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x)) iff s in dom(f*reproj(i,x)) proof let s be Element of G.i; s in dom((r(#)f)*reproj(i,x)) iff reproj(i,x).s in dom(r(#)f) by A3,FUNCT_1:11; hence thesis by A1,A3,FUNCT_1:11; end; then A4: for s be object holds s in dom(r(#)(f*reproj(i,x))) iff s in dom((r(#)f)*reproj(i,x)) by A2; then A4a:dom(r(#)(f*reproj(i,x))) =dom((r(#)f)*reproj(i,x)) by TARSKI:2; A5:for s be Element of G.i holds s in dom((r(#)f)*reproj(i,x)) iff reproj(i,x).s in dom(r(#)f) proof let s be Element of G.i; dom(reproj(i,x))=the carrier of G.i by FUNCT_2:def 1; hence thesis by FUNCT_1:11; end; for z being Element of G.i st z in dom(r(#)(f*reproj(i,x))) holds (r(#)(f*reproj(i,x))).z = ((r(#)f)*reproj(i,x)).z proof let z be Element of G.i; assume A6: z in dom(r(#)(f*reproj(i,x))); then A7: z in dom(f*reproj(i,x)) by VFUNCT_1:def 4; A9: f/.(reproj(i,x).z) = f.(reproj(i,x).z) by A1,A5,A4a,A6,PARTFUN1:def 6 .= (f*reproj(i,x)).z by A7,FUNCT_1:12 .= (f*reproj(i,x))/.z by A7,PARTFUN1:def 6; A10:(r(#)(f*reproj(i,x))).z =(r(#)(f*reproj(i,x)))/.z by A6,PARTFUN1:def 6 .= r * f/.(reproj(i,x).z) by A6,A9,VFUNCT_1:def 4; ((r(#)f)*reproj(i,x)).z = (r(#)f).(reproj(i,x).z) by A2,A4b,A6,FUNCT_1:12 .= (r(#)f)/.(reproj(i,x).z) by A5,A4a,A6,PARTFUN1:def 6 .= r * f/.(reproj(i,x).z) by A5,A4a,A6,VFUNCT_1:def 4; hence thesis by A10; end; hence thesis by A4,TARSKI:2,PARTFUN1:5; end; theorem for i be set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds f1+f2 is_partial_differentiable_in x,i & partdiff(f1+f2,x,i)=partdiff(f1,x,i)+partdiff(f2,x,i) proof let i0 be set; set i=In(i0,dom G); assume A1: i0 in dom G; then A2:(f1+f2)*reproj(i,x) = f1*reproj(i,x)+f2*reproj(i,x) by Th26; assume A3: f1 is_partial_differentiable_in x,i0 & f2 is_partial_differentiable_in x,i0; hence f1+f2 is_partial_differentiable_in x,i0 by A2,NDIFF_1:35; thus partdiff(f1,x,i0)+partdiff(f2,x,i0) = diff(f1*reproj(i,x)+f2*reproj(i,x),proj(i).x) by A3,NDIFF_1:35 .= partdiff((f1+f2),x,i0) by A1,Th26; end; theorem for i be set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds f1-f2 is_partial_differentiable_in x,i & partdiff(f1-f2,x,i)=partdiff(f1,x,i)-partdiff(f2,x,i) proof let i0 be set; assume A1: i0 in dom G; set i=In(i0,dom G); assume A2: f1 is_partial_differentiable_in x,i0 & f2 is_partial_differentiable_in x,i0; (f1-f2)*reproj(i,x) = f1*reproj(i,x)-f2*reproj(i,x) by A1,Th26; hence f1-f2 is_partial_differentiable_in x,i0 by A2,NDIFF_1:36; thus partdiff(f1,x,i0)-partdiff(f2,x,i0) = diff(f1*reproj(i,x)-f2*reproj(i,x),proj(i).x) by A2,NDIFF_1:36 .= partdiff((f1-f2),x,i0) by A1,Th26; end; theorem for i be set st i in dom G & f is_partial_differentiable_in x,i holds r(#)f is_partial_differentiable_in x,i & partdiff((r(#)f),x,i) = r*partdiff(f,x,i) proof let i0 be set; assume A1: i0 in dom G; set i=In(i0,dom G); assume A2: f is_partial_differentiable_in x,i0; r(#)(f*reproj(i,x)) = (r(#)f)*reproj(i,x) by A1,Th27; hence r(#)f is_partial_differentiable_in x,i0 by A2,NDIFF_1:37; thus partdiff(r(#)f,x,i0) = diff(r(#)(f*reproj(i,x)),proj(i).x) by A1,Th27 .= r*partdiff(f,x,i0) by A2,NDIFF_1:37; end; begin :: Continuously differentiable and Partial derivative theorem Th31: ||. proj(i).x .|| <= ||.x.|| proof reconsider y= x as Element of product carr G by Th10; proj(i).x = y.i by Def3; hence thesis by PRVECT_2:10; end; registration let G be RealNormSpace-Sequence; cluster -> (len G)-element for Point of product G; coherence proof let x be Point of product G; A1: the carrier of (product G) = product carr G by Th10; A2: dom x = dom (carr G) & for i be set st i in dom (carr G) holds x.i in carr G.i by A1,CARD_3:9; len carr G = len G by PRVECT_2:def 4; then dom x= Seg len G by A2,FINSEQ_1:def 3; then len x = len G by FINSEQ_1:def 3; hence thesis by CARD_1:def 7; end; end; theorem Th32: for G be RealNormSpace-Sequence, T be RealNormSpace, i be set, Z be Subset of product G, f be PartFunc of product G,T st Z is open holds f is_partial_differentiable_on Z,i iff Z c=dom f & for x be Point of product G st x in Z holds f is_partial_differentiable_in x,i proof let G be RealNormSpace-Sequence, T be RealNormSpace, i0 be set, Z be Subset of product G, f be PartFunc of product G,T; assume A1: Z is open; set i = In(i0,dom G); set S=G.i; set RNS= R_NormSpace_of_BoundedLinearOperators(S,T); hereby assume A2: f is_partial_differentiable_on Z,i0; hence Z c=dom f; let nx0 be Point of product G; reconsider x0=proj(i).nx0 as Point of S; assume A4: nx0 in Z; then f|Z is_partial_differentiable_in nx0,i0 by A2; then consider N0 being Neighbourhood of x0 such that A5: N0 c= dom((f|Z)*reproj(i,nx0)) and A6: ex L be Point of RNS,R be RestFunc of S,T st for x be Point of S st x in N0 holds ((f|Z)*reproj(i,nx0))/.x-((f|Z)*reproj(i,nx0))/.x0 = L .( x-x0)+R/.(x-x0) by NDIFF_1:def 6; consider L be Point of RNS,R be RestFunc of S,T such that A7: for x be Point of S st x in N0 holds ((f|Z)*reproj(i,nx0))/.x - ((f|Z)*reproj(i,nx0))/.x0 = L.(x-x0) + R/.(x-x0) by A6; consider N1 being Neighbourhood of x0 such that A8: for x be Point of S st x in N1 holds (reproj(i,nx0)).x in Z by A1,A4,Th23; A9:now let x be Point of S; assume x in N1; then (reproj(i,nx0)).x in Z by A8; then (reproj(i,nx0)).x in (dom f) /\ Z by A2,XBOOLE_0:def 4; hence (reproj(i,nx0)).x in dom(f|Z) by RELAT_1:61; end; reconsider N = N0 /\ N1 as Neighbourhood of x0 by Th8; (f|Z)*reproj(i,nx0) c= f*reproj(i,nx0) by RELAT_1:29,59; then A10:dom((f|Z)*reproj(i,nx0)) c= dom(f*reproj(i,nx0)) by RELAT_1:11; N c= N0 by XBOOLE_1:17; then A11:N c= dom(f*reproj(i,nx0)) by A5,A10; A12:dom(reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1; now let x be Point of S; assume x in N; then A13: x in N0 & x in N1 by XBOOLE_0:def 4; then A14: (reproj(i,nx0)).x in dom(f|Z) by A9; then A15: (reproj(i,nx0)).x in dom f & (reproj(i,nx0)).x in Z by RELAT_1:57; A16: (reproj(i,nx0)).x0 in dom(f|Z) by A9,NFCONT_1:4; then A17: (reproj(i,nx0)).x0 in dom f & (reproj(i,nx0)).x0 in Z by RELAT_1:57; A18: ((f|Z)*reproj(i,nx0))/.x = (f|Z)/.(reproj(i,nx0)/.x) by A14,A12,PARTFUN2:4 .= f/.(reproj(i,nx0)/.x) by A15,PARTFUN2:17 .= (f*reproj(i,nx0))/.x by A12,A15,PARTFUN2:4; ((f|Z)*reproj(i,nx0))/.x0 = (f|Z)/.(reproj(i,nx0)/.x0) by A12,A16,PARTFUN2:4 .= f/.(reproj(i,nx0)/.x0) by A17,PARTFUN2:17 .= (f*reproj(i,nx0))/.x0 by A12,A17,PARTFUN2:4; hence (f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0 =L.(x-x0)+R/.(x-x0) by A7,A13,A18; end; hence f is_partial_differentiable_in nx0,i0 by A11,NDIFF_1:def 6; end; assume that A19:Z c=dom f and A20:for nx be Point of product G st nx in Z holds f is_partial_differentiable_in nx,i0; now let nx0 be Point of product G; assume A21: nx0 in Z; then A22:f is_partial_differentiable_in nx0,i0 by A20; reconsider x0=proj(i).nx0 as Point of S; consider N0 being Neighbourhood of x0 such that N0 c= dom (f*reproj(i,nx0)) and A23: ex L be Point of RNS,R be RestFunc of S,T st for x be Point of S st x in N0 holds (f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0 = L.(x-x0)+R /.(x-x0) by A22,NDIFF_1:def 6; consider N1 being Neighbourhood of x0 such that A24: for x be Point of S st x in N1 holds (reproj(i,nx0)).x in Z by A1,A21,Th23; A25:now let x be Point of S; assume x in N1; then (reproj(i,nx0)).x in Z by A24; then (reproj(i,nx0)).x in (dom f) /\ Z by A19,XBOOLE_0:def 4; hence (reproj(i,nx0)).x in dom(f|Z) by RELAT_1:61; end; A26:N1 c= dom((f|Z)*reproj(i,nx0)) proof let z be object; assume A27:z in N1; then z in the carrier of S; then A28: z in dom (reproj(i,nx0)) by FUNCT_2:def 1; reconsider x=z as Point of S by A27; (reproj(i,nx0)).x in dom(f|Z) by A27,A25; hence z in dom((f|Z)*reproj(i,nx0)) by A28,FUNCT_1:11; end; reconsider N=N0 /\ N1 as Neighbourhood of x0 by Th8; N c= N1 by XBOOLE_1:17; then A29:N c= dom((f|Z)*reproj(i,nx0)) by A26; consider L be Point of RNS,R be RestFunc of S,T such that A30: for x be Point of S st x in N0 holds (f*reproj(i,nx0))/.x-(f*reproj(i,nx0))/.x0=L.(x-x0)+R/.(x-x0) by A23; now let x be Point of S; assume A31: x in N; then A32: x in N0 by XBOOLE_0:def 4; A33: dom (reproj(i,nx0)) = the carrier of G.i by FUNCT_2:def 1; x in N1 by A31,XBOOLE_0:def 4; then A34: (reproj(i,nx0)).x in dom(f|Z) by A25; then A35: (reproj(i,nx0)).x in dom f /\ Z by RELAT_1:61; then A36: (reproj(i,nx0)).x in dom f by XBOOLE_0:def 4; A37: (reproj(i,nx0)).x0 in dom(f|Z) by A25,NFCONT_1:4; then A38: (reproj(i,nx0)).x0 in dom f /\ Z by RELAT_1:61; then A39: (reproj(i,nx0)).x0 in dom f by XBOOLE_0:def 4; A40: ((f|Z)*reproj(i,nx0))/.x = (f|Z)/. (reproj(i,nx0)/.x ) by A34,A33,PARTFUN2:4 .= f/. (reproj(i,nx0)/.x) by A35,PARTFUN2:16 .= (f*reproj(i,nx0))/.x by A33,A36,PARTFUN2:4; ((f|Z)*reproj(i,nx0))/.x0 = (f|Z)/. (reproj(i,nx0)/.x0 ) by A33,A37,PARTFUN2:4 .= f/. (reproj(i,nx0)/.x0) by A38,PARTFUN2:16 .= (f*reproj(i,nx0))/.x0 by A33,A39,PARTFUN2:4; hence ((f|Z)*reproj(i,nx0))/.x -((f|Z)*reproj(i,nx0))/.x0 = L.(x-x0)+R/.(x-x0) by A40,A32,A30; end; hence (f|Z) is_partial_differentiable_in nx0,i0 by A29,NDIFF_1:def 6; end; hence thesis by A19; end; theorem Th33: for i,j be Element of dom G, x be Point of G.i, z be Element of product carr G st z= reproj(i,0.(product G)).x holds (i = j implies z.j = x) & (i <> j implies z.j = 0.(G.j)) proof let i,j be Element of dom G, x be Point of G.i, z be Element of product carr G; assume A1: z= reproj(i,0.(product G)).x; reconsider Zr = 0.(product G) as Element of product carr G by Th10; reconsider ixr = (reproj(i,0.(product G))).x as Element of product carr G by Th10; A2:reproj(i,0.(product G)).x = 0.(product G) +* (i,x) by Def4; set ix= i .--> x; consider g be Function such that A3: Zr = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; A4:dom Zr = dom G by A3,Lm1; now assume i <> j; then z.j = Zr.j by A1,A2,FUNCT_7:32; hence z.j = 0.(G.j) by Th14; end; hence thesis by A1,A2,A4,FUNCT_7:31; end; theorem Th34: for x,y be Point of G.i holds reproj(i,0.(product G)).(x+y) = reproj(i,0.(product G)).x + reproj(i,0.(product G)).y proof let x,y be Point of G.i; reconsider v=reproj(i,0.(product G)).(x+y) as Element of product carr G by Th10; reconsider s=reproj(i,0.(product G)).x as Element of product carr G by Th10; reconsider t=reproj(i,0.(product G)).y as Element of product carr G by Th10; for j be Element of dom G holds v.j=s.j + t.j proof let j be Element of dom G; per cases; suppose A1: i= j; then reconsider yy=y as Point of G.j; v.j = x+y by Th33,A1; then v.j =s.j + yy by Th33,A1; hence v.j =s.j + t.j by Th33,A1; end; suppose A2: i <> j; then v.j = 0.(G.j) by Th33; then v.j = 0.(G.j) + 0.(G.j) by RLVECT_1:def 4; then v.j =s.j + 0.(G.j) by Th33,A2; hence v.j =s.j + t.j by Th33,A2; end; end; hence thesis by Th12; end; theorem Th35: for x,y be Point of product G holds proj(i).(x+y) = proj(i).x + proj(i).y proof let x,y be Point of product G; reconsider v=x+y as Element of product carr G by Th10; reconsider s=x as Element of product carr G by Th10; reconsider t=y as Element of product carr G by Th10; proj(i).(x+y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3; hence thesis by Th12; end; theorem for x,y be Point of G.i holds reproj(i,0.(product G)).(x-y) = reproj(i,0.(product G)).x - reproj(i,0.(product G)).y proof let x,y be Point of G.i; reconsider v=reproj(i,0.(product G)).(x-y) as Element of product carr G by Th10; reconsider s=reproj(i,0.(product G)).x as Element of product carr G by Th10; reconsider t=reproj(i,0.(product G)).y as Element of product carr G by Th10; for j be Element of dom G holds v.j=s.j - t.j proof let j be Element of dom G; per cases; suppose A1: i= j; then reconsider yy=y as Point of G.j; v.j = x-y by Th33,A1; then v.j =s.j - yy by Th33,A1; hence v.j =s.j - t.j by Th33,A1; end; suppose A2: i <> j; then v.j = 0.(G.j) by Th33; then v.j = 0.(G.j) - 0.(G.j) by RLVECT_1:13; then v.j =s.j - 0.(G.j) by Th33,A2; hence v.j =s.j - t.j by Th33,A2; end; end; hence thesis by Th15; end; theorem Th37: for x,y be Point of product G holds proj(i).(x-y) = proj(i).x - proj(i).y proof let x,y be Point of product G; reconsider v=x-y as Element of product carr G by Th10; reconsider s=x as Element of product carr G by Th10; reconsider t=y as Element of product carr G by Th10; proj(i).(x-y)= v.i & proj(i).x = s.i & proj(i).y = t.i by Def3; hence thesis by Th15; end; theorem Th38: for x be Point of G.i st x <> 0.(G.i) holds reproj(i,0.(product G)).x <> 0.(product G) proof let x be Point of G.i; assume A1: x <> 0.(G.i); assume A2: reproj(i,0.(product G)).x = 0.(product G); reconsider v=reproj(i,0.(product G)).x as Element of product carr G by Th10; x = v.i by Th33; hence contradiction by A1,Th14,A2; end; theorem Th39: for x be Point of G.i, a be Real holds reproj(i,0.(product G)).(a*x) = a*(reproj(i,0.(product G)).x) proof let x be Point of G.i,a be Real; reconsider a as Real; reconsider v=reproj(i,0.(product G)).(a*x) as Element of product carr G by Th10; reconsider s=reproj(i,0.(product G)).x as Element of product carr G by Th10; for j be Element of dom G holds v.j=a*(s.j) proof let j be Element of dom G; per cases; suppose A1: i= j; then v.j = a*x by Th33; hence v.j =a*(s.j) by Th33,A1; end; suppose A2: i <> j; then v.j = 0.(G.j) by Th33; then v.j = a*0.(G.j) by RLVECT_1:10; hence v.j =a*(s.j) by Th33,A2; end; end; hence thesis by Th13; end; theorem Th40: for x be Point of product G,a be Real holds proj(i).(a*x) = a*(proj(i).x) proof let x be Point of product G,a be Real; reconsider a as Real; reconsider v=a*x as Element of product carr G by Th10; reconsider s=x as Element of product carr G by Th10; proj(i).(a*x)= v.i & proj(i).x = s.i by Def3; hence thesis by Th13; end; theorem Th41: for G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G, S, x be Point of product G, i be set st f is_differentiable_in x holds f is_partial_differentiable_in x,i & partdiff(f,x,i) = diff(f,x) * reproj(In(i,dom G),0.(product G)) proof let G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G, S, x be Point of product G, i0 be set; assume A1: f is_differentiable_in x; set i=In(i0,dom G); consider N being Neighbourhood of x such that A2: N c= dom f & ex R be RestFunc of product G,S st for y be Point of product G st y in N holds f/.y-f/.x = diff(f,x).(y-x) + R/.(y-x) by A1,NDIFF_1:def 7; consider R be RestFunc of product G,S such that A3: for y be Point of product G st y in N holds f/.y-f/.x = diff(f,x).(y-x) + R/.(y-x) by A2; consider r0 be Real such that A4: 0 < r0 & {z where z is Point of product G : ||. z-x .|| < r0} c= N by NFCONT_1:def 1; set u = f*reproj(i,x); reconsider x0 = proj(i).x as Point of G.i; set Z=0.(product G); set Nx0 = {z where z is Point of G.i: ||. z-x0 .|| < r0 }; now let s be object; assume s in Nx0; then ex z be Point of G.i st s=z & ||. z-x0 .|| < r0; hence s in the carrier of G.i; end; then Nx0 is Subset of G.i by TARSKI:def 3; then reconsider Nx0 as Neighbourhood of x0 by A4,NFCONT_1:def 1; A5:for xi be Element of G.i st xi in Nx0 holds reproj(i,x).xi in N proof let xi be Element of G.i; assume xi in Nx0; then A6: ex z be Point of G.i st xi=z & ||. z-x0 .|| < r0; reproj(i,x).xi-x = reproj(i,Z).(xi-x0) by Th22; then ||. reproj(i,x).xi-x .|| < r0 by Th21,A6; then reproj(i,x).xi in {z where z is Point of product G : ||. z-x .|| < r0 }; hence thesis by A4; end; A7:R is total by NDIFF_1:def 5; then A8:dom R = the carrier of product G by PARTFUN1:def 2; reconsider R1 = R*reproj(i,0.(product G)) as PartFunc of G.i,S; A9: dom(reproj(i,0.(product G))) = the carrier of G.i by FUNCT_2:def 1; A10: dom R1 = the carrier of G.i by A7,PARTFUN1:def 2; for r be Real st r > 0 ex d be Real st d > 0 & for z be Point of G.i st z <> 0.(G.i) & ||.z.|| < d holds (||.z.||" * ||. R1/.z .||) < r proof let r be Real; assume r > 0; then consider d be Real such that A11: d > 0 & for z be Point of product G st z <> 0.(product G ) & ||.z.|| < d holds (||.z.||" * ||. R/.z .||) < r by A7,NDIFF_1:23; take d; now let z be Point of G.i; assume A12: z <> 0.(G.i) & ||.z.|| < d; A13: ||. reproj(i,Z).z .|| = ||.z.|| by Th21; R/.(reproj(i,Z).z) = R.(reproj(i,Z).z) by A8,PARTFUN1:def 6; then R/.(reproj(i,Z).z) =R1.z by A9,FUNCT_1:13; then R/.(reproj(i,Z).z) =R1/.z by A10,PARTFUN1:def 6; hence ||.z.||" * ||. R1/.z .|| < r by A11,A13,A12,Th38; end; hence thesis by A11; end; then reconsider R1 as RestFunc of G.i,S by A7,NDIFF_1:23; reconsider dfx = diff(f,x) as Lipschitzian LinearOperator of product G,S by LOPBAN_1:def 9; reconsider LD1 = dfx*reproj(i,0.(product G )) as Function of G.i,S; A14: now let x,y be Element of G.i; LD1.(x+y) = dfx.(reproj(i,Z).(x+y)) by FUNCT_2:15; then LD1.(x+y) =dfx.(reproj(i,Z).x+reproj(i,Z).y) by Th34; then LD1.(x+y) =dfx.(reproj(i,Z).x)+dfx.(reproj(i,Z).y) by VECTSP_1:def 20; then LD1.(x+y) =LD1.x+dfx.(reproj(i,Z).y) by FUNCT_2:15; hence LD1.(x+y) =LD1.x+LD1.y by FUNCT_2:15; end; now let x be Element of G.i, a be Real; LD1.(a*x) = dfx.(reproj(i,Z).(a*x)) by FUNCT_2:15; then LD1.(a*x) = dfx.(a*(reproj(i,Z).x)) by Th39; then LD1.(a*x) =a*dfx.(reproj(i,Z).x) by LOPBAN_1:def 5; hence LD1.(a*x) =a*LD1.x by FUNCT_2:15; end; then reconsider LD1 as LinearOperator of G.i,S by A14,LOPBAN_1:def 5,VECTSP_1:def 20; consider K0 being Real such that A15: 0 <= K0 & for x being VECTOR of product G holds ||. dfx.x .|| <= K0 * ||. x .|| by LOPBAN_1:def 8; now let r being VECTOR of G.i; ||. dfx.(reproj(i,Z).r) .|| <= K0 * ||. reproj(i,Z).r .|| by A15; then ||. dfx.(reproj(i,Z).r ) .|| <= K0 * ||.r.|| by Th21; hence ||. LD1.r .|| <= K0 * ||.r.|| by FUNCT_2:15; end; then LD1 is Lipschitzian by A15; then reconsider LD1 as Point of R_NormSpace_of_BoundedLinearOperators(G.i,S) by LOPBAN_1:def 9; now let s be object; assume s in (reproj(i,x)).:Nx0; then ex t being Element of G.i st t in Nx0 & s = (reproj(i,x)).t by FUNCT_2:65; hence s in dom f by A2,A5; end; then A16: (reproj(i,x)).:Nx0 c= dom f; dom(reproj(i,x)) = the carrier of G.i by FUNCT_2:def 1; then A17: Nx0 c= dom u by A16,FUNCT_3:3; A18: for y be Point of G.i st y in Nx0 holds u/.y-u/.x0 = LD1.(y-x0) + R1/.(y-x0) proof let y be Point of G.i; assume A19: y in Nx0; then A20:reproj(i,x).y in N by A5; A21: reproj(i,x).x0 = x +* (i,x0) by Def4; A22: the carrier of (product G) = product carr G by Th10; x.i=x0 by Def3,A22; then A23:x= x +* (i,x0) by FUNCT_7:35; A24:reproj(i,x).x0 in N by A5,NFCONT_1:4; u/.y = u.y by A19,A17,PARTFUN1:def 6; then u/.y = f.(reproj(i,x).y) by FUNCT_2:15; then A25:u/.y = f/.(reproj(i,x).y) by A20,A2,PARTFUN1:def 6; R/.(reproj(i,Z).(y-x0)) = R.(reproj(i,Z).(y-x0)) by A8,PARTFUN1:def 6; then R/.(reproj(i,Z).(y-x0)) = R1.(y-x0) by A9,FUNCT_1:13; then A26:R/.(reproj(i,Z).(y-x0)) = R1/.(y-x0) by A10,PARTFUN1:def 6; x0 in Nx0 by NFCONT_1:4; then u/.x0 = u.x0 by A17,PARTFUN1:def 6; then u/.x0 = f.(reproj(i,x).x0) by FUNCT_2:15; then u/.y-u/.x0 = f/.(reproj(i,x).y) -f/.x by A25,A23,A24,A2,A21,PARTFUN1:def 6; then u/.y-u/.x0 = diff(f,x).(reproj(i,x).y-x) + R/.(reproj(i,x).y-x) by A3,A19,A5; then u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,x).y-x) by Th22; then u/.y-u/.x0 = dfx.(reproj(i,Z).(y-x0)) + R/.(reproj(i,Z).(y-x0)) by Th22; hence u/.y-u/.x0 = LD1.(y-x0) + R1/.(y-x0) by A26,FUNCT_2:15; end; hence f is_partial_differentiable_in x,i0 by A17,NDIFF_1:def 6; u is_differentiable_in x0 by A17,A18,NDIFF_1:def 6; hence thesis by A17,A18,NDIFF_1:def 7; end; Lm5: for G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G,S, x be Point of product G ex L be Lipschitzian LinearOperator of product G,S st for h be Element of product G ex w be FinSequence of S st dom w = Seg len G & (for i be Element of NAT st i in Seg len G holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).h) ) & L.h=Sum w proof let G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G,S, x be Point of product G; set m=len G; defpred LX[set,set] means ex w be FinSequence of S st dom w = Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).\$1) ) & \$2=Sum w; A1:for v being Element of product G holds ex y be Element of S st LX[v,y] proof let v being Element of product G; defpred YX[set,set] means ex i be Element of NAT st i=\$1 & \$2 = partdiff(f,x,i).(proj(In(i,dom G)).v); A2: for i be Nat st i in Seg m holds ex r being Element of S st YX[i,r] proof let i be Nat; assume i in Seg m; reconsider i0=i as Element of NAT by ORDINAL1:def 12; partdiff(f,x,i0).(proj(In(i0,dom G)).v) in the carrier of S; hence thesis; end; consider w be FinSequence of S such that A3: dom w = Seg m & for i be Nat st i in Seg m holds YX[i,w.i] from FINSEQ_1:sch 5(A2); A4: now let i be Element of NAT; assume i in Seg m; then YX[i,w.i] by A3; hence w.i = partdiff(f,x,i).(proj(In(i,dom G)).v); end; reconsider w0 = Sum w as Element of S; ex w be FinSequence of S st dom w=Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).v)) & w0 = Sum w by A4,A3; hence ex y0 be Element of S st LX[v,y0]; end; consider L being Function of product G,S such that A5: for h being Element of product G holds LX[h,L.h] from FUNCT_2:sch 3(A1); A6:for s,t being Element of product G holds L.(s+t) = L.s + L.t proof let s,t being Element of product G; consider w be FinSequence of S such that A7: dom w=Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).s)) & L.s = Sum w by A5; consider v be FinSequence of S such that A8: dom v=Seg m & (for i be Element of NAT st i in Seg m holds v.i = partdiff(f,x,i).(proj(In(i,dom G)).t )) & L.t = Sum v by A5; consider u be FinSequence of S such that A9: dom u=Seg m & (for i be Element of NAT st i in Seg m holds u.i = partdiff(f,x,i).(proj(In(i,dom G)).(s+t))) & L.(s+t) = Sum u by A5; A10: len w = m by A7,FINSEQ_1:def 3; A11: len v = m by A8,FINSEQ_1:def 3; A12: len u = m by A9,FINSEQ_1:def 3; now let i be Nat; assume A13: i in dom w; then A14: 1 <= i & i <= m by A7,FINSEQ_1:1; then w/.i = w.i by A10,FINSEQ_4:15; then A15: w/.i = partdiff(f,x,i).(proj(In(i,dom G)).s) by A7,A13; v/.i = v.i by A14,A11,FINSEQ_4:15; then A16: v/.i = partdiff(f,x,i).(proj(In(i,dom G)).t) by A7,A8,A13; A17: partdiff(f,x,i) is Lipschitzian LinearOperator of G.(In(i,dom G)),S by LOPBAN_1:def 9; u.i = partdiff(f,x,i).(proj(In(i,dom G)).(s+t)) by A7,A9,A13; then u.i = partdiff(f,x,i).(proj(In(i,dom G)).s + proj(In(i,dom G)).t) by Th35; hence u.i = w/.i + v/.i by A15,A16,A17,VECTSP_1:def 20; end; hence L.(s+t) = L.s + L.t by A9,A7,A8,A10,A11,A12,RLVECT_2:2; end; for s being Element of product G, r being Real holds L.(r*s) = r*(L.s) proof let s being Element of product G, r being Real; consider w be FinSequence of S such that A18: dom w = Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).s)) & L.s = Sum w by A5; consider u be FinSequence of S such that A19: dom u = Seg m & (for i be Element of NAT st i in Seg m holds u.i = partdiff(f,x,i).(proj(In(i,dom G)).(r*s)) ) & L.(r*s) = Sum u by A5; A20: len w = m & len u = m by A18,A19,FINSEQ_1:def 3; now let i be Nat; assume A21: i in dom w; then 1 <= i & i <= m by A18,FINSEQ_1:1; then w/.i = w.i by A20,FINSEQ_4:15; then A22: w/.i = partdiff(f,x,i).(proj(In(i,dom G)).s ) by A18,A21; A23: partdiff(f,x,i) is Lipschitzian LinearOperator of G.(In(i,dom G)),S by LOPBAN_1:def 9; u.i = partdiff(f,x,i).(proj(In(i,dom G)).(r*s)) by A18,A19,A21; then u.i = partdiff(f,x,i).(r*proj(In(i,dom G)).s) by Th40; hence u.i = r*(w/.i) by A22,A23,LOPBAN_1:def 5; end; hence L.(r*s) = r * L.s by A18,A19,A20,RLVECT_2:3; end; then reconsider L as LinearOperator of product G,S by A6,LOPBAN_1:def 5,VECTSP_1:def 20; defpred YXL[set,set] means ex i be Element of NAT st i=\$1 & \$2 = ||. partdiff(f,x,i) .||; A24: for i be Nat st i in Seg m holds ex r being Element of REAL st YXL[i,r] proof let i be Nat; assume i in Seg m; reconsider i0=i as Element of NAT by ORDINAL1:def 12; reconsider r = ||. partdiff(f,x,i0) .|| as Element of REAL; YXL[i,r]; hence thesis; end; consider Kw be FinSequence of REAL such that A25: dom Kw=Seg m & for i be Nat st i in Seg m holds YXL[i,Kw.i] from FINSEQ_1:sch 5(A24); A26:now let i be Element of NAT; assume i in Seg m; then YXL[i,Kw.i] by A25; hence Kw.i = ||. partdiff(f,x,i) .||; end; A27: now let i be Nat; assume i in dom Kw; then Kw.i = ||. partdiff(f,x,i) .|| by A26,A25; hence 0 <= Kw.i; end; set LK= Sum Kw; for s being Element of product G holds ||. L.s .|| <= LK*||. s .|| proof let s being Element of product G; consider w be FinSequence of S such that A29: dom w=Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).s)) & L.s = Sum w by A5; defpred YXD[set,set] means ex i be Element of NAT st i=\$1 & \$2 = ||.partdiff(f,x,i).|| * ||.s.||; A30:for i be Nat st i in Seg m holds ex r being Element of REAL st YXD[i,r] proof let i be Nat; assume i in Seg m; reconsider i0=i as Element of NAT by ORDINAL1:def 12; reconsider r = ||.partdiff(f,x,i0).|| * ||.s.|| as Element of REAL by XREAL_0:def 1; YXD[i,r]; hence thesis; end; consider Dw be FinSequence of REAL such that A31:dom Dw=Seg m & for i be Nat st i in Seg m holds YXD[i,Dw.i] from FINSEQ_1:sch 5(A30); A32:now let i be Element of NAT; assume i in Seg m; then YXD[i,Dw.i] by A31; hence Dw.i = ||.partdiff(f,x,i).|| * ||.s.||; end; defpred YXH[set,set] means ex i be Element of NAT st i=\$1 & \$2 = ||. w/.i .||; A33:for i be Nat st i in Seg m holds ex r being Element of REAL st YXH[i,r] proof let i be Nat; assume i in Seg m; reconsider i0=i as Element of NAT by ORDINAL1:def 12; reconsider r = ||. w/.i0 .|| as Element of REAL; YXH[i,r]; hence thesis; end; consider yseq be FinSequence of REAL such that A34: dom yseq=Seg m & for i be Nat st i in Seg m holds YXH[i,yseq.i] from FINSEQ_1:sch 5(A33); A35: now let i be Element of NAT; assume i in Seg m; then YXH[i,yseq.i] by A34; hence yseq.i = ||. w/.i .||; end; len w = len yseq by A29,A34,FINSEQ_3:29; then A36: ||.L.s.|| <= Sum yseq by A29,A35,Th7; m = len yseq by A34,FINSEQ_1:def 3; then A37: yseq is Element of m-tuples_on REAL by FINSEQ_2:92; len Dw = m by A31,FINSEQ_1:def 3; then A38:Dw is Element of m-tuples_on REAL by FINSEQ_2:92; now let i be Nat; assume A39: i in Seg m; then A40: yseq.i = ||. w/.i .|| by A35; w/.i = w.i by A39,A29,PARTFUN1:def 6; then A41: ||. w/.i .|| = ||.partdiff(f,x,i).(proj(In(i,dom G)).s) .|| by A29,A39; reconsider DF1=partdiff(f,x,i) as Lipschitzian LinearOperator of G.(In(i,dom G)),S by LOPBAN_1:def 9; A42: ||. DF1.(proj(In(i,dom G)).s) .|| <= ||.partdiff(f,x,i).|| * ||.(proj(In(i,dom G)).s) .|| by LOPBAN_1:32; product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; then reconsider ss= s as Element of product carr G; reconsider xi = proj(In(i,dom G)).s as Point of G.(In(i,dom G)); xi = ss.(In(i,dom G)) by Def3; then ||.partdiff(f,x,i).|| * ||.(proj(In(i,dom G)).s) .|| <=||.partdiff(f,x,i).|| * ||.s.|| by PRVECT_2:10,XREAL_1:64; then ||. w/.i .|| <= ||.partdiff(f,x,i).|| * ||.s.|| by A41,A42,XXREAL_0:2; hence yseq.i <= Dw.i by A32,A39,A40; end; then A43: Sum yseq <= Sum Dw by A37,A38,RVSUM_1:82; len Kw = m by A25,FINSEQ_1:def 3; then reconsider KKw= Kw as Element of m-tuples_on REAL by FINSEQ_2:92; (||.s.|| * KKw) in m-tuples_on REAL; then ex t be Element of REAL* st t= (||.s.|| * KKw) & len t = m; then A44: dom Dw = dom (||.s.|| * Kw) by A31,FINSEQ_1:def 3; now let k be Nat; assume A45: k in dom Dw; then Dw.k = ||.partdiff(f,x,k).|| * ||.s.|| by A32,A31; then Dw.k = ||.s.|| * Kw.k by A26,A45,A31; hence Dw.k = (||.s.|| * Kw).k by RVSUM_1:45; end; then Dw = ||.s.|| * Kw by A44,FINSEQ_1:13; then Sum Dw = (Sum Kw)* ||.s.|| by RVSUM_1:87; hence thesis by A36,A43,XXREAL_0:2; end; then reconsider L as Lipschitzian LinearOperator of product G,S by A27,RVSUM_1:84,LOPBAN_1:def 8; take L; thus thesis by A5; end; theorem Th42: for S be RealNormSpace, h,g be FinSequence of S st len h = len g + 1 & (for i be Nat st i in dom g holds g/.i = h /.i - h/.(i+1)) holds h /.1 - h/.(len h) = Sum g proof let S be RealNormSpace, h,g be FinSequence of S; assume that A1: len h = len g + 1 and A2: for i be Nat st i in dom g holds g/.i = h/.i - h/.(i+1); consider F be sequence of the carrier of S such that A3: Sum g = F.(len g) & F.0 = 0.S & for j be Nat,v be Element of S st j < len g & v = g.(j + 1) holds F.(j + 1) = F.j + v by RLVECT_1:def 12; per cases; suppose len g = 0; hence thesis by A3,A1,RLVECT_1:15; end; suppose A4:len g > 0; defpred P[Nat] means \$1 <= len g implies F.\$1 = h/.1 - h/.(\$1+1); A5: P[1] proof assume A6: 1 <= len g; then 1 in Seg len g; then A7: 1 in dom g by FINSEQ_1:def 3; reconsider zz0=0 as Element of NAT; g/.1 = g.( zz0 + 1 ) by A7,PARTFUN1:def 6; then F.(zz0 + 1) = F.0 + g/.1 by A3,A6 .= g/.1 by A3,RLVECT_1:4; hence F.1 = h/.1 - h/.(1+1) by A7,A2; end; A8: for j be Nat st 1 <= j holds P[j] implies P[j+1] proof let j be Nat; assume 1 <= j; assume A9: P[j]; assume A10:j+1 <= len g; then A12: j+1 in dom g by XREAL_1:38,FINSEQ_3:25; then A13: g.(j+1)=g/.(j+1) by PARTFUN1:def 6; F.(j+1) = F.j + g/.(j+1) by A13,A10,A3,NAT_1:13 .=F.j + (h/.(j+1) - h/.(j+1+1)) by A2,A12 .= h/.1 - h/.(j+1) + h/.(j+1) - h/.(j+1+1) by A9,A10,NAT_1:13,RLVECT_1:28 .= h/.1 -(h/.(j+1) - h/.(j+1)) - h/.(j+1+1) by RLVECT_1:29 .= h/.1 -0.S - h/.(j+1+1) by RLVECT_1:15; hence thesis by RLVECT_1:13; end; A14:1 <= len g by A4,NAT_1:14; for i be Nat st 1 <= i holds P[i] from NAT_1:sch 8(A5,A8); hence thesis by A3,A1,A14; end; end; theorem for G be RealNormSpace-Sequence, x,y be Element of product carr G, Z be set holds x +* (y|Z) is Element of product carr G by CARD_3:79; theorem Th44: for G be RealNormSpace-Sequence, x,y be Point of product G, Z,x0 be Element of product carr G, X be set st Z=0.(product G) & x0=x & y= Z +* (x0|X) holds ||.y.|| <= ||.x.|| proof let G be RealNormSpace-Sequence, x,y be Point of product G, Z,x0 be Element of product carr G, X be set; assume A1: Z=0.(product G) & x0=x & y= Z +* (x0|X); reconsider y0 = y as Element of product carr G by Th10; A2: ||.y.|| = (productnorm G).y by PRVECT_2:def 13 .= |. normsequence(G,y0) .| by PRVECT_2:def 12; A3: ||.x.|| = (productnorm G).x by PRVECT_2:def 13 .= |. normsequence(G,x0) .| by A1,PRVECT_2:def 12; reconsider Ny = normsequence(G,y0) as (len G)-element FinSequence of REAL; reconsider Nx = normsequence(G,x0) as (len G)-element FinSequence of REAL; A4:len Nx = len G & len Ny = len G by CARD_1:def 7; for k be Element of NAT st k in Seg len Ny holds 0 <= Ny.k & Ny.k <= Nx.k proof let k be Element of NAT; assume A5: k in Seg len Ny; then reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3; x0 is Element of the carrier of (product G) by Th10; then reconsider xx = x0 as (len G)-element FinSequence; dom xx = Seg len G by FINSEQ_1:89; then A6: k in dom x0 by A5,CARD_1:def 7; reconsider yk = y0.k1, xk = x0.k1 as Element of the carrier of (G.k1); A7: Nx.k = (the normF of G.k1).(x0.k1) by PRVECT_2:def 11; A8: Ny.k = ||. yk .|| by PRVECT_2:def 11; hence 0 <= Ny.k; A9: Nx.k = ||. xk .|| by PRVECT_2:def 11; per cases; suppose k1 in X; then A10: k1 in dom(x0|X) by A6,RELAT_1:57; then y0.k1 = (x0|X).k1 by A1,FUNCT_4:13; then y0.k1 = x0.k1 by A10,FUNCT_1:47; hence Ny.k <= Nx.k by A7,PRVECT_2:def 11; end; suppose not k1 in X; then not k1 in dom(x0|X); then y0.k1 = Z.k1 by A1,FUNCT_4:11; then y0.k1 = 0.(G.k1) by A1,Th14; hence Ny.k <= Nx.k by A8,A9; end; end; hence ||.y.|| <= ||.x.|| by A2,A3,A4,PRVECT_2:2; end; theorem Th45: for G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G, S, x,y be Point of product G ex h be FinSequence of product G, g be FinSequence of S, Z,y0 be Element of product carr G st y0=y & Z = 0.(product G) & len h = len G + 1 & len g = len G & (for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i))) & (for i be Nat st i in dom g holds g/.i = f/.(x+h/.i) - f/.(x+h/.(i+1))) & (for i be Nat, hi be Point of product G st i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||) & f /.(x+y) - f/.x = Sum g proof let G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G,S, x,y be Point of product G; set m= len G; A1: the carrier of (product G) = product carr G by Th10; reconsider Z0 = 0.(product G) as Element of product carr G by Th10; reconsider y0 = y as Element of product carr G by Th10; reconsider y1=y as (len G)-element FinSequence; reconsider Z1=0.(product G) as (len G)-element FinSequence; len y1 = m by CARD_1:def 7; then A2:dom y1 = dom G by FINSEQ_3:29; len Z1 = m by CARD_1:def 7; then A3:dom Z1 = dom G by FINSEQ_3:29; defpred H[Nat,set] means \$2=Z0 +* (y0| Seg (len G + 1-'\$1)); A4:for k be Nat st k in Seg(m+1) ex x being Element of product G st H[k,x] proof let k be Nat; assume k in Seg(m+1); Z0 +* (y0| Seg (len G + 1-'k)) is Element of product carr G by CARD_3:79; hence thesis by A1; end; consider h be FinSequence of product G such that A5: dom h = Seg(m+1) & for j being Nat st j in Seg(m+1) holds H[j,h.j] from FINSEQ_1:sch 5(A4); A6:now let j being Nat; assume A7: j in dom h; then h/.j = h.j by PARTFUN1:def 6; hence h/.j = Z0 +* (y0| Seg (len G + 1-'j)) by A7,A5; end; deffunc Z(Nat)=f/.(x+h/.\$1); consider z be FinSequence of S such that A8: len z = m+1 & for j being Nat st j in dom z holds z.j = Z(j) from FINSEQ_2:sch 1; A9:now let j being Nat; assume A10: j in dom z; then z/.j = z.j by PARTFUN1:def 6; hence z/.j = f/.(x+h/.j) by A10,A8; end; deffunc G(Nat) = z/.\$1 - z/.(\$1+1); consider g be FinSequence of S such that A11:len g = m & for j being Nat st j in dom g holds g.j = G(j) from FINSEQ_2:sch 1; A12:now let j being Nat; assume A13: j in dom g; then g/.j = g.j by PARTFUN1:def 6; hence g/.j = z/.j - z /.(j+1) by A13,A11; end; A14:m+1-'1 = m+1-1 by NAT_1:11,XREAL_1:233; reconsider zz0=0 as Element of NAT; 1 <= m+1 by NAT_1:11; then A15:1 in dom h by A5; then h/.1 = Z0 +* (y0| Seg (len G + 1-'1)) by A6 .= Z0 +* (y0| dom G) by A14,FINSEQ_1:def 3 .= Z0 +* y0 by A2; then A16:h/.1 = y by A2,A3,FUNCT_4:19; A17:m+1-'(len z) = m+1 - len z by A8,XREAL_1:233; 1 <= len z & len z <= m+1 by A8,NAT_1:14; then A18:len z in dom h by A5; then A19:h/.(len z) = Z0 +* (y0| Seg 0) by A6,A17,A8 .=0.(product G); A20:dom h= dom z by A5,A8,FINSEQ_1:def 3; then A21:z/.1 = f/.(x+y) by A9,A16,A15; z/.(len z) = f/. (x+h/.(len z)) by A9,A20,A18; then A22:z/.(len z) = f/.x by A19,RLVECT_1:def 4; take h,g,Z0,y0; A23:now let i be Nat; assume A24: i in dom g; then A25:i in Seg m by A11,FINSEQ_1:def 3; then 1 <= i & i <= m by FINSEQ_1:1; then A26:i+1 <= m+1 by XREAL_1:6; Seg m c= Seg (m+1) by NAT_1:11,FINSEQ_1:5; then A27:z/.i =f/.(x+h/.i) by A9,A5,A25,A20; 1 <= i+1 by NAT_1:11; then i+1 in Seg (m+1) by A26; then i+1 in dom z by A8,FINSEQ_1:def 3; then z/.(i+1) =f /. (x+h/.(i+1)) by A9; hence g/.i = f /. (x+h/.i) - f /.(x+h/.(i+1)) by A12,A24,A27; end; now let i be Nat, hi be Element of product G; assume A28: i in dom h & h/.i= hi; then h/.i = Z0 +* (y0| Seg (len G + 1-'i)) by A6; hence ||. hi .|| <=||. y .|| by Th44,A28; end; hence thesis by A6,A21,A22,A23,A8,A12,Th42,A5,A11,FINSEQ_1:def 3; end; theorem Th46: for G be RealNormSpace-Sequence, i be Element of dom G, x,y be Point of product G, xi be Point of G.i st y = reproj(i,x).xi holds proj(i).y = xi proof let G be RealNormSpace-Sequence, i be Element of dom G, x,y be Point of product G, xi be Point of G.i; assume A1: y = reproj(i,x).xi; A2:y = x +* (i,xi) by A1,Def4; x in the carrier of product G; then x in product carr G by Th10; then consider g being Function such that A3:x = g & dom g = dom carr G & for y be object st y in dom carr G holds g.y in (carr G).y by CARD_3:def 5; A4:i in dom G; A5:i in dom x by Lm1,A4,A3; y is Element of product carr G by Th10; then proj(i).y = (x +* (i,xi)).i by A2,Def3; hence proj(i).y = xi by A5,FUNCT_7:31; end; theorem Th47: for G be RealNormSpace-Sequence, i be Element of dom G, y be Point of product G, q be Point of G.i st q = proj(i).y holds y = reproj(i,y).q proof let G be RealNormSpace-Sequence, i be Element of dom G, y be Point of product G, q be Point of G.i; assume A1: q = proj(i).y; reconsider z1 = reproj(i,y).q as (len G)-element FinSequence; reconsider z2 = y as (len G)-element FinSequence; A2:dom z1 = Seg len G by FINSEQ_1:89 .= dom z2 by FINSEQ_1:89; for k be Nat st k in dom z1 holds z1.k = z2.k proof let k be Nat; assume k in dom z1; product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; then A3: q = y.i by A1,Def3; per cases; suppose A4: k = i; then (y +*(i,q)).k = q by A3,FUNCT_7:35; hence z1.k = z2.k by A4,A3,Def4; end; suppose k <> i; then (y +*(i,q)).k = y.k by FUNCT_7:32; hence z1.k = z2.k by Def4; end; end; hence thesis by A2,FINSEQ_1:13; end; theorem Th48: for G be RealNormSpace-Sequence, i be Element of dom G, x,y be Point of product G, xi be Point of G.i st y = reproj(i,x).xi holds reproj(i,x)=reproj(i,y) proof let G be RealNormSpace-Sequence, i be Element of dom G, x,y be Point of product G, xi be Point of G.i; assume A1: y = reproj(i,x).xi; for v be Element of G.i holds reproj(i,x).v = reproj(i,y).v proof let v be Element of G.i; A2: reproj(i,x).v = x +* (i,v) & reproj(i,y).v = y +* (i,v) by Def4; reconsider xv = reproj(i,x).v, yv = reproj(i,y).v as (len G)-element FinSequence; A3: dom xv = Seg len G & dom yv = Seg len G by FINSEQ_1:89; then A4: dom xv = dom G by FINSEQ_1:def 3; for k be Nat st k in dom xv holds xv.k = yv.k proof let k be Nat; assume A5: k in dom xv; x in the carrier of product G & y in the carrier of product G; then A6: x in product carr G & y in product carr G by Th10; then consider g be Function such that A7: x = g & dom g = dom carr G & for i be object st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; consider g1 be Function such that A8: y = g1 & dom g1 = dom carr G & for i be object st i in dom carr G holds g1.i in (carr G).i by A6,CARD_3:def 5; A9: k in dom y & k in dom x by A7,A8,Lm1,A5,A4; per cases; suppose k = i; then (y +*(i,v)).k = v & (x +*(i,v)).k = v by A9,FUNCT_7:31; hence yv.k = xv.k by A2; end; suppose A10: k <> i; A11: yv.k = y.k & xv.k = x.k by A2,A10,FUNCT_7:32; y = x +* (i,xi) by A1,Def4; hence yv.k = xv.k by A11,A10,FUNCT_7:32; end; end; hence reproj(i,x).v = reproj(i,y).v by A3,FINSEQ_1:13; end; hence thesis; end; theorem Th49: for G be RealNormSpace-Sequence, i,j be Element of dom G, x,y be Point of product G, xi be Point of G.i st y = reproj(i,x).xi & i <> j holds proj(j).x = proj(j).y proof let G be RealNormSpace-Sequence, i,j be Element of dom G, x,y be Point of product G, xi be Point of G.i; assume A1: y = reproj(i,x).xi & i <> j; reconsider y1 = y as Element of product carr G by Th10; A2:y = x +* (i,xi) by A1,Def4; set ix = i .--> xi; A3: the carrier of (product G) = product carr G by Th10; y1.j = x.j by A2,A1,FUNCT_7:32; then proj(j).y = x.j by Def3; hence thesis by A3,Def3; end; theorem for G be RealNormSpace-Sequence, F be RealNormSpace, i be Element of dom G, x be Point of product G, xi be Point of G.i, f be PartFunc of product G,F, g be PartFunc of G.i,F st proj(i).x=xi & g=f*reproj(i,x) holds diff(g,xi) = partdiff(f,x,i) proof let G be RealNormSpace-Sequence, F be RealNormSpace, i be Element of dom G, x be Point of product G, xi be Point of G.i, f be PartFunc of product G,F, g be PartFunc of G.i,F; i=In(i,dom G) by SUBSET_1:def 8; hence thesis; end; theorem Th51: for G be RealNormSpace-Sequence, F be RealNormSpace, f be PartFunc of product G,F, x be Point of product G, i be set, M be Real, L be Point of R_NormSpace_of_BoundedLinearOperators (G.(In(i,dom G)),F), p,q be Point of G.(In(i,dom G)) st i in dom G & (for h be Point of G.(In(i,dom G)) st h in ]. p,q .[ holds ||. partdiff(f,reproj(In(i,dom G),x).h,i) - L .|| <= M) & (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds reproj(In(i,dom G),x).h in dom f) & (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds f is_partial_differentiable_in (reproj(In(i,dom G),x).h),i) holds ||.f/.(reproj(In(i,dom G),x).q) - f/.(reproj(In(i,dom G),x).p) - L.(q-p) .|| <= M * ||.q-p.|| proof let G be RealNormSpace-Sequence, F be RealNormSpace, f be PartFunc of product G,F, x be Point of product G, i be set, M be Real, L be Point of R_NormSpace_of_BoundedLinearOperators (G.(In(i,dom G)),F), p,q be Point of G.(In(i,dom G)); assume A1: i in dom G & (for h be Point of G.(In(i,dom G)) st h in ]. p,q .[ holds ||. partdiff(f,reproj(In(i,dom G),x).h,i) - L .|| <= M) & (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds reproj(In(i,dom G),x).h in dom f ) & (for h be Point of G.(In(i,dom G)) st h in [. p,q .] holds f is_partial_differentiable_in (reproj(In(i,dom G),x).h),i ); per cases ; suppose B2: p=q ; set S = G.(In(i,dom G)) ; reconsider LL=L as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9; B3: L.(0.S) = LL.(0 * 0.S) by RLVECT_1:10 .= 0 * LL.(0.S) by LOPBAN_1:def 5 .= 0.F by RLVECT_1:10 ; B4: ||.f/.(reproj(In(i,dom G),x).q) - f/.(reproj(In(i,dom G),x).p) - L.(q-p) .|| = ||. 0.F - L.(q-p) .|| by B2,RLVECT_1:15 .= ||. 0.F - L.(0.S) .|| by B2,RLVECT_1:15 .= ||. 0.F .|| by B3,RLVECT_1:13 .= 0; M*||. q-p .|| = M * ||. 0.S .|| by B2,RLVECT_1:15 .= 0 ; hence thesis by B4; end; suppose ASM: p<>q ; set m=len G; set S=G.(In(i,dom G)); set g=f*reproj(In(i,dom G),x); A2:now let h be object; assume A3: h in [. p,q .]; then reconsider h1=h as Point of S; A4: dom reproj(In(i,dom G),x) = the carrier of S by FUNCT_2:def 1; reproj(In(i,dom G),x).h1 in dom f by A1,A3; hence h in dom g by A4,FUNCT_1:11; end; then A5:[. p,q .] c= dom g; A6:now let x0 be Point of S; assume A7: x0 in [. p,q .]; set y=reproj(In(i,dom G),x).x0; A8: proj(In(i,dom G)).y = x0 by Th46; f is_partial_differentiable_in y,i by A1,A7; hence g is_differentiable_in x0 by A8,Th48; end; X1: ]. p,q .[ = { p+t*(q-p) where t is Real : 0 < t & t < 1} by ASM,LMOPN; now let z be object; assume z in ].p,q.[; then consider z1 be Real such that A9: z=p+z1*(q-p) & 0 < z1 & z1 < 1 by X1; z = (1-z1)*p+z1*q by A9,Lm2; then z in {(1-r1)*p + r1*q where r1 is Real : 0 <= r1 & r1 <= 1 } by A9; hence z in [. p,q .] by RLTOPSP1:def 2; end; then A10:for x be Point of S st x in ].p,q.[ holds g is_differentiable_in x by A6; A11:for x be Point of S st x in [.p,q.] holds g is_continuous_in x by A6,NDIFF_1:44; A12:now let h be Point of S; set y=reproj(In(i,dom G),x).h; assume h in ]. p,q .[; then A13: ||. partdiff(f,y,i) - L .|| <= M by A1; proj(In(i,dom G)).y = h by Th46; hence ||. diff(g,h) - L .|| <= M by A13,Th48; end; A14:p in dom g & q in dom g by A2,RLTOPSP1:68; f/.(reproj(In(i,dom G),x).p) = f/.(reproj(In(i,dom G),x)/.p) & f/.(reproj(In(i,dom G),x).q) = f/.(reproj(In(i,dom G),x)/.q); then f/.(reproj(In(i,dom G),x).p) = g/.p & f/.(reproj(In(i,dom G),x).q) = g/.q by A14,PARTFUN2:3; hence ||.f/.(reproj(In(i,dom G),x).q) - f/.(reproj(In(i,dom G),x).p) - L.(q-p) .|| <= M * ||.q-p.|| by A12,Th20,A5,A10,A11; end; end; theorem Th52: for G be RealNormSpace-Sequence, x,y,z,w be Point of product G, i be Element of dom G, d be Real, p,q,r be Point of G.i st ||. y-x .|| < d & ||. z-x .|| < d & p= proj(i).y & z=reproj(i,y).q & r in [. p,q .] & w= reproj(i,y).r holds ||. w-x .|| < d proof let G be RealNormSpace-Sequence, x,y,z,w be Point of product G, i be Element of dom G, d be Real, p,q,r be Point of G.i; assume that A1: ||. y-x .|| < d & ||. z-x .|| < d and A2: p= proj(i).y & z=reproj(i,y).q and A3: r in [. p,q .] and A4: w= reproj(i,y).r; set wx = w-x; set yx = y-x; set zx = z-x; reconsider xi = proj(i).x as Point of G.i; r in {(1-t)*p + t*q where t is Real: 0 <= t & t <= 1 } by A3,RLTOPSP1:def 2; then consider t be Real such that A5: r = (1-t)*p + t*q & 0 <= t & t <= 1; A6: r = p + t*(q-p) & 0 <= t & t <= 1 by A5,Lm2; reconsider wx0 = wx, yx0 = yx, zx0 = zx as Element of product carr G by Th10; reconsider Nwx = normsequence(G,wx0) as (len G)-element FinSequence of REAL; reconsider Nyx = normsequence(G,yx0) as (len G)-element FinSequence of REAL; reconsider Nzx = normsequence(G,zx0) as (len G)-element FinSequence of REAL; set tyz = (1-t)*yx + t*zx; reconsider tyz0 = tyz as Element of product carr G by Th10; reconsider Ntyz = normsequence(G,tyz0) as (len G)-element FinSequence of REAL; A7:1 = 1-t+t; r = p + (t*q - t*p) by A6,RLVECT_1:34 .= (p + -t*p) + t*q by RLVECT_1:def 3 .= (1*p - t*p) + t*q by RLVECT_1:def 8 .= (1-t)*p + t*q by RLVECT_1:35; then A8:r-xi = (1-t)*p + t*q - 1*xi by RLVECT_1:def 8 .= (1-t)*p + t*q - ((1-t)*xi + t*xi) by A7,RLVECT_1:def 6 .= (1-t)*p + t*q - t*xi - (1-t)*xi by RLVECT_1:27 .= (1-t)*p +(t*q - t*xi) - (1-t)*xi by RLVECT_1:28 .= (t*q - t*xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:def 3 .= t*(q-xi) + ((1-t)*p - (1-t)*xi) by RLVECT_1:34 .= t*(q-xi) + (1-t)*(p-xi) by RLVECT_1:34; reconsider Swx = wx as (len G)-element FinSequence; reconsider Syz = (1-t)*yx + t*zx as (len G)-element FinSequence; A9:dom Swx = Seg len G & dom Syz = Seg len G by FINSEQ_1:89; A10:for k be Nat st k in dom Swx holds Swx.k = Syz.k proof let k be Nat; assume k in dom Swx; then reconsider k0 = k as Element of dom G by A9,FINSEQ_1:def 3; per cases; suppose A11: k = i; then Swx.k = proj(i).wx0 by Def3; then A12: Swx.k = proj(i).w - proj(i).x by Th37; A13: proj(i).z = q by A2,Th46; Syz.k = proj(i).tyz0 by A11,Def3; then Syz.k = proj(i).((1-t)*yx) + proj(i).(t*zx) by Th35; then Syz.k = (1-t)*(proj(i).yx) + proj(i).(t*zx) by Th40; then Syz.k = (1-t)*(proj(i).yx) + t*proj(i).zx by Th40; then Syz.k = (1-t)*(proj(i).y - proj(i).x) + t*proj(i).zx by Th37; then Syz.k = (1-t)*(p-xi) + t*(q-xi) by A2,A13,Th37; hence Swx.k = Syz.k by A12,A8,A4,Th46; end; suppose k <> i; then A14: proj(k0).y = proj(k0).w & proj(k0).z = proj(k0).y by A2,A4,Th49; Swx.k = proj(k0).wx0 by Def3; then A15: Swx.k = proj(k0).w - proj(k0).x by Th37; Syz.k = proj(k0).tyz0 by Def3 .= proj(k0).((1-t)*yx) + proj(k0).(t*zx) by Th35 .= (1-t)*(proj(k0).yx) + proj(k0).(t*zx) by Th40 .= (1-t)*(proj(k0).yx) + t*proj(k0).zx by Th40; then Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*proj(k0).zx by Th37; then Syz.k = (1-t)*(proj(k0).y - proj(k0).x) + t*(proj(k0).y - proj(k0).x) by A14,Th37; then Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x + t*(proj(k0).y - proj(k0).x) by RLVECT_1:34; then Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x + (t*proj(k0).y - t*proj(k0).x) by RLVECT_1:34; then Syz.k = (1-t)*proj(k0).y - (1-t)*proj(k0).x + t*proj(k0).y - t*proj(k0).x by RLVECT_1:def 3; then Syz.k = (1-t)*proj(k0).y - ((1-t)*proj(k0).x - t*proj(k0).y) - t*proj(k0).x by RLVECT_1:29; then Syz.k = (1-t)*proj(k0).y + (t*proj(k0).y + - (1-t)*proj(k0).x) - t*proj(k0).x by RLVECT_1:33; then Syz.k = (1-t)*proj(k0).y + t*proj(k0).y + - (1-t)*proj(k0).x - t*proj(k0).x by RLVECT_1:def 3; then Syz.k = ((1-t)+t)*proj(k0).y + - (1-t)*proj(k0).x - t*proj(k0).x by RLVECT_1:def 6; then Syz.k = proj(k0).y + - (1-t)*proj(k0).x - t*proj(k0).x by RLVECT_1:def 8; then Syz.k = proj(k0).y + (- (1-t)*proj(k0).x - t*proj(k0).x) by RLVECT_1:28; then Syz.k = proj(k0).y + (- (t*proj(k0).x + (1-t)*proj(k0).x)) by RLVECT_1:30; then Syz.k = proj(k0).y + (- (t+(1-t))*proj(k0).x) by RLVECT_1:def 6; hence Swx.k = Syz.k by A15,A14,RLVECT_1:def 8; end; end; A16:len Nwx = len G & len Ntyz = len G by CARD_1:def 7; for k be Element of NAT st k in Seg len Nwx holds 0 <= Nwx.k & Nwx.k <= Ntyz.k proof let k be Element of NAT; assume A17: k in Seg len Nwx; then reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3; reconsider wxk = wx0.k1 as Element of (G.k1); A18: Nwx.k = ||. wxk .|| by PRVECT_2:def 11; wx0.k1 = Syz.k by A10,A17,A16,A9; hence thesis by A18,PRVECT_2:def 11; end; then A19: |. Nwx .| <= |. Ntyz .| by A16,PRVECT_2:2; A20: ||. w-x .|| = (productnorm G).wx by PRVECT_2:def 13; ||. (1-t)*yx + t*zx .|| = (productnorm G).tyz by PRVECT_2:def 13 .= |. normsequence(G,tyz0) .| by PRVECT_2:def 12; then A21: ||. w-x .|| <= ||. (1-t)*yx + t*zx .|| by A19,A20,PRVECT_2:def 12; A22: ||. (1-t)*yx + t*zx .|| <= |.1-t.|*||. y-x .|| + |.t.|*||. z-x .|| by NORMSP_1:5; A23: |.1-t.| = 1-t & |.t.| = t by A5,ABSVALUE:def 1,XREAL_1:48; |.1-t.|*||. y-x .|| + |.t.|*||. z-x .|| < d proof per cases; suppose t=1 or t=0; hence thesis by A1,A23; end; suppose t<>1 & t<>0; then 0 < t & t < 1 by A5,XXREAL_0:1; then 0 < t & 1-t > 0 by XREAL_1:50; then |.1-t.|*||. y-x .|| < (1-t)*d & |.t.|*||. z-x .|| < t*d by A1,A23,XREAL_1:68; then |.1-t.|*||. y-x .|| + |.t.|*||. z-x .|| < (1-t)*d + t*d by XREAL_1:8; hence thesis; end; end; then ||. (1-t)*yx + t*zx .|| < d by A22,XXREAL_0:2; hence ||. w-x .|| < d by A21,XXREAL_0:2; end; theorem Th53: for G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G,S, X be Subset of product G, x,y,z be Point of product G, i be set, p,q be Point of G.(In(i,dom G)), d,r be Real st i in dom G & X is open & x in X & ||. y-x .|| < d & ||. z-x .|| < d & X c= dom f & (for x be Point of product G st x in X holds f is_partial_differentiable_in x,i) & (for z be Point of product G st ||. z-x .|| < d holds z in X) & (for z be Point of product G st ||. z-x .|| < d holds ||. partdiff(f,z,i) - partdiff(f,x,i).|| <=r) & z = reproj(In(i,dom G),y).p & q = proj(In(i,dom G)).y holds ||. f/.z - f/.y - ((partdiff(f,x,i)).(p-q)) .|| <= ||. p-q .||*r proof let G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G,S, X be Subset of product G, x,y,z be Point of product G, i0 be set, p,q be Point of G.(In(i0,dom G)), d,r be Real; assume A1: i0 in dom G & X is open & x in X & ||. y-x .|| < d & ||. z-x .|| < d & X c= dom f & (for x be Point of product G st x in X holds f is_partial_differentiable_in x,i0) & (for z be Point of product G st ||. z-x .|| < d holds z in X) & (for z be Point of product G st ||. z-x .|| < d holds ||. partdiff(f,z,i0) - partdiff(f,x,i0).|| <=r) & z = reproj(In(i0,dom G),y).p & q = proj(In(i0,dom G)).y; set i=In(i0,dom G); A2:y = reproj(i,y).q by A1,Th47; A3:now let h be Point of G.i; assume h in [. q,p .]; then ||. reproj(i,y).h - x .|| < d by A1,Th52; hence reproj(i,y).h in dom f by A1; end; A4:now let h be Point of G.i; assume h in [. q,p .]; then ||. reproj(i,y).h - x .|| < d by A1,Th52; hence f is_partial_differentiable_in (reproj(i,y).h),i0 by A1; end; for h be Point of G.i st h in ]. q,p .[ holds ||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0) .|| <=r proof let h be Point of G.i; assume A5: h in ]. q,p .[; ].q,p.[ c= [. q,p .] by XBOOLE_1:36; then ||. reproj(i,y).h - x .|| < d by A1,A5,Th52; hence ||. partdiff(f,reproj(i,y).h,i0) - partdiff(f,x,i0).|| <=r by A1; end; hence thesis by A2,A1,Th51,A3,A4; end; theorem Th54: for G be RealNormSpace-Sequence, h be FinSequence of product G, y,x be Point of product G, y0,Z be Element of product carr G, j be Element of NAT st y=y0 & Z=0.(product G) & len h = (len G)+1 & 1 <= j & j <= len G & (for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i))) holds x + h/.j = reproj(In((len G)+1-'j,dom G),(x+h/.(j+1))) .(proj(In((len G)+1-'j,dom G)).(x+y)) proof let G be RealNormSpace-Sequence, h be FinSequence of product G, y,x be Point of product G, y0,Z be Element of product carr G, j be Element of NAT; assume that A1: y = y0 and A2: Z = 0.(product G) and A3: len h = len G + 1 and A4: 1 <= j & j <= len G and A5: for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg(len G + 1-'i)); len G <= len h by A3,NAT_1:11; then j <= len h by A4,XXREAL_0:2; then j in Seg len h by A4; then j in dom h by FINSEQ_1:def 3; then A6:h/.j = Z +* (y0| Seg(len G + 1 -'j)) by A5; 1 <= j+1 & j+1 <= len h by A3,A4,NAT_1:12,XREAL_1:6; then j+1 in Seg len h; then j+1 in dom h by FINSEQ_1:def 3; then A7:h/.(j+1) = Z +* (y0| Seg(len G + 1-'(j+1))) by A5; j in Seg len G by A4; then len G -'j + 1 in Seg len G by NAT_2:6; then len G + 1 -' j in Seg len G by A4,NAT_D:38; then len G + 1 -' j in dom G by FINSEQ_1:def 3; then A8:In((len G)+1-'j,dom G) = len G + 1 -' j by SUBSET_1:def 8; set xh = x+h/.(j+1); reconsider x1 = x, y1 = y as Element of product carr G by Th10; reconsider xy = x + y as Element of product carr G by Th10; xh is Element of product carr G by Th10; then consider g being Function such that A9:xh = g & dom g = dom carr G & for y be object st y in dom carr G holds g.y in (carr G).y by CARD_3:def 5; A10:dom xh = dom G by A9,Lm1; proj(In((len G)+1-'j,dom G)).(x+y) = xy.(len G + 1 -' j) by A8,Def3; then A11:reproj(In((len G)+1-'j,dom G),(x+h/.(j+1))) .(proj(In((len G)+1-'j,dom G)).(x+y)) = xh +* (In((len G)+1-'j,dom G), xy.(len G + 1 -' j)) by Def4 .= xh +* (In((len G)+1-'j,dom G) .--> xy.(len G + 1 -' j)) by A10,FUNCT_7:def 3 .= xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j)) by A8,FUNCOP_1:def 9; reconsider F1 = x + h/.j as (len G)-element FinSequence; reconsider F2 = reproj(In((len G)+1-'j,dom G),(x+h/.(j+1))) .(proj(In((len G)+1-'j,dom G)).(x+y)) as (len G)-element FinSequence; reconsider h1 = h/.j as Element of product carr G by Th10; reconsider xh1 = x + h/.j as Element of product carr G by Th10; reconsider h2 = h/.(j+1) as Element of product carr G by Th10; A12:len F1 = len G & len F2 = len G by CARD_1:def 7; for k be Nat st 1 <= k & k <= len F1 holds F1.k = F2.k proof let k be Nat; assume A13: 1 <= k & k <= len F1; then A14: k in Seg len F1; then reconsider k1 = k as Element of dom G by CARD_1:def 7,FINSEQ_1:def 3; proj(k1).xh1 = proj(k1).x + proj(k1).(h/.j) by Th35; then A15: F1.k = proj(k1).x + proj(k1).(h/.j) by Def3; y0 is Element of the carrier of product G by Th10; then A16: dom y0 = Seg len G by FINSEQ_1:89; A17: proj(k1).(h/.j) = h1.k by Def3; A18: dom(y0|Seg(len G + 1-'j)) = dom y0 /\ Seg (len G + 1 -' j) by RELAT_1:61; A19: the carrier of (product G) = product carr G by Th10; per cases; suppose A20: not k in Seg(len G + 1 -' j); then not k in dom(y0|Seg(len G +1 -'j)) by A18,XBOOLE_0:def 4; then proj(k1).(h/.j) = Z.k by A17,A6,FUNCT_4:11; then A21: proj(k1).(h/.j) = proj(k1).(0.(product G)) by A2,Def3; not 1 <= k or not k <= len G + 1 -' j by A20; then not k in dom ({len G + 1 -'j} --> xy.(len G + 1 -' j)) by A13,TARSKI:def 1; then (xh +* ({len G + 1 -'j} --> xy.(len G + 1 -' j))).k1 = xh.k1 by FUNCT_4:11; then A22: F2.k = proj(k1).(x+h/.(j+1)) by A19,A11,Def3; A23: proj(k1).(h/.(j+1)) = h2.k by Def3; len G + 1-'(j+1) <= len G +1-'j by NAT_1:11,NAT_D:41; then Seg(len G +1-'(j+1)) c= Seg(len G +1-'j) by FINSEQ_1:5; then not k in Seg(len G+1-'(j+1)) by A20; then not k in dom y0 /\ Seg(len G +1-'(j+1)) by XBOOLE_0:def 4; then not k in dom(y0|Seg(len G+1-'(j+1))) by RELAT_1:61; then (Z +* (y0| Seg(len G + 1-'(j+1)))).k = Z.k by FUNCT_4:11; then proj(k1).(h/.(j+1)) = proj(k1).(0.(product G)) by A2,A23,A7,Def3; hence F1.k = F2.k by A21,A15,A22,Th35; end; suppose A24: k in Seg(len G + 1 -' j); then A25: k in dom(y0|Seg(len G +1 -' j)) by A18,A14,A16,A12,XBOOLE_0:def 4; then proj(k1).(h/.j) = (y0|Seg(len G +1-'j)).k by A17,A6,FUNCT_4:13; then proj(k1).(h/.j) = y0.k by A25,FUNCT_1:47; then A26: proj(k1).(h/.j) = proj(k1).y by A1,Def3; then A27: F1.k = proj(k1).(x+y) by A15,Th35; per cases; suppose A28: k = len G + 1 -' j; A29: k in {k} by TARSKI:def 1; then k in dom({k} --> xy.k) by FUNCOP_1:13; then ( xh +* ({k} --> xy.k)).k1 = ({k} --> xy.k).k by FUNCT_4:13; then F2.k = xy.k by A11,A29,A28,FUNCOP_1:7; hence F1.k = F2.k by A27,Def3; end; suppose A30: k <> len G + 1 -' j; then not k in dom({len G + 1 -'j} --> xy.(len G +1 -'j)) by TARSKI:def 1; then F2.k = xh.k by A11,FUNCT_4:11; then A31: F2.k = proj(k1).(x+h/.(j+1)) by A19,Def3; k <= len G + 1 -' j by A24,FINSEQ_1:1; then k < len G + 1 -' j by A30,XXREAL_0:1; then k <= len G + 1 -' j -' 1 by NAT_D:49; then k <= len G + 1 -' (j+1) by NAT_2:30; then k in Seg (len G+1-'(j+1)) by A13; then A32: k in dom(y0| Seg(len G + 1-'(j+1))) by A14,A16,A12,RELAT_1:57; proj(k1).(h/.(j+1)) = h2.k by Def3; then proj(k1).(h/.(j+1)) = (y0| Seg(len G + 1-'(j+1))).k1 by A7,A32,FUNCT_4:13; then proj(k1).(h/.(j+1)) = y0.k by A32,FUNCT_1:47; then proj(k1).(h/.(j+1)) = proj(k1).y by A1,Def3; hence F1.k = F2.k by A26,A15,A31,Th35; end; end; end; hence thesis by A12; end; theorem Th55: for G be RealNormSpace-Sequence, h be FinSequence of product G, y,x be Point of product G, y0,Z be Element of product carr G, j be Element of NAT st y=y0 & Z=0.(product G) & len h = (len G)+1 & 1 <= j & j <= len G & (for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i))) holds (proj(In((len G)+1-'j,dom G)).(x+y)) - proj(In((len G)+1-'j,dom G)).(x+h/.(j+1)) = (proj(In((len G)+1-'j,dom G)).y) proof let G be RealNormSpace-Sequence, h be FinSequence of product G, y,x be Point of product G, y0,Z be Element of product carr G, j be Element of NAT; assume that A1: y = y0 and A2: Z=0.(product G) and A3: len h = (len G)+1 & 1 <= j & j <= len G and A4: for i be Nat st i in dom h holds h/.i=Z +* (y0| Seg (len G + 1-'i)); x + h/.j = reproj(In((len G)+1-'j,dom G),(x+h/.(j+1))) .(proj(In((len G)+1-'j,dom G)).(x+y)) by A1,A2,A3,A4,Th54; then proj(In((len G)+1-'j,dom G)).(x+h/.j) = proj(In((len G)+1-'j,dom G)).(x+y) by Th46; then A5:proj(In((len G)+1-'j,dom G)).(x+y) - proj(In((len G)+1-'j,dom G)).(x+h/.(j+1)) = proj(In((len G)+1-'j,dom G)).(x + h/.j - (x+h/.(j+1))) by Th37; x + h/.j - (x + h/.(j+1)) = h/.j + x - x - h/.(j+1) by RLVECT_1:27 .= h/.j + (x - x) - h/.(j+1) by RLVECT_1:28 .= h/.j + 0.(product G) - h/.(j+1) by RLVECT_1:15 .= h/.j - h/.(j+1) by RLVECT_1:4; then A6:proj(In((len G)+1-'j,dom G)).(x+y) - proj(In((len G)+1-'j,dom G)).(x+h/.(j+1)) = proj(In((len G)+1-'j,dom G)).(h/.j) - proj(In((len G)+1-'j,dom G)).(h/.(j+1)) by A5,Th37; y0 is Element of the carrier of product G by Th10; then A7:dom y0 = Seg len G by FINSEQ_1:89; j in Seg len G by A3; then len G -'j + 1 in Seg len G by NAT_2:6; then A8:len G + 1 -' j in Seg len G by A3,NAT_D:38; A9:j < len G +1 by A3,NAT_1:13; then len G+1-'j in Seg(len G+1-'j) by FINSEQ_1:3,NAT_D:36; then A10:len G+1-'j in dom (y0|Seg(len G+1-'j)) by A7,A8,RELAT_1:57; len G+1-'j = len G+1-'(j+1)+1 by A9,NAT_2:7; then A11:len G+1-'(j+1) < len G+1-'j by NAT_1:13; dom (y0|Seg(len G+1-'(j+1))) c= Seg(len G+1-'(j+1)) by RELAT_1:58; then A12:not len G+1-'j in dom (y0|Seg(len G+1-'(j+1))) by A11,FINSEQ_1:1; reconsider h1 = h/.j as Element of product carr G by Th10; reconsider h2 = h/.(j+1) as Element of product carr G by Th10; j in Seg len h by A3,A9; then j in dom h by FINSEQ_1:def 3; then A13:h/.j = Z +* (y0|Seg(len G+1-'j)) by A4; len G + 1 -' j in dom G by A8,FINSEQ_1:def 3; then A14:In((len G)+1-'j,dom G) = len G + 1 -' j by SUBSET_1:def 8; then A15:proj(In((len G)+1-'j,dom G)).(h/.j) = h1.(len G+1-'j) by Def3 .= (y0|Seg(len G+1-'j)).(len G+1-'j) by A10,A13,FUNCT_4:13 .= y0.(len G +1-'j) by A10,FUNCT_1:47 .= proj(In(len G+1-'j,dom G)).y by A1,A14,Def3; 1 <= j+1 & j+1 <= len h by A3,NAT_1:12,XREAL_1:6; then j+1 in Seg len h; then j+1 in dom h by FINSEQ_1:def 3; then A16:h/.(j+1) = Z +* (y0|Seg(len G+1-'(j+1))) by A4; proj(In((len G)+1-'j,dom G)).(h/.(j+1)) = h2.(len G+1-'j) by A14,Def3 .= Z.(len G+1-'j) by A16,A12,FUNCT_4:11 .= proj(In(len G+1-'j,dom G)).(0.(product G)) by A14,A2,Def3; hence proj(In((len G)+1-'j,dom G)).(x+y) - proj(In((len G)+1-'j,dom G)).(x+h/.(j+1)) = proj(In(len G+1-'j,dom G)).(y - 0.(product G)) by A6,A15,Th37 .= proj(In(len G+1-'j,dom G)).y by RLVECT_1:13; end; theorem Th56: for G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G, S, X be Subset of product G, x be Point of product G st X is open & x in X & (for i be set st i in dom G holds f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X) holds f is_differentiable_in x & for h be Point of product G ex w be FinSequence of S st dom w = dom G & (for i be set st i in dom G holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).h)) & diff(f,x).h = Sum w proof let G be RealNormSpace-Sequence, S be RealNormSpace, f be PartFunc of product G, S, X be Subset of product G, x be Point of product G; assume A1: X is open & x in X & (for i be set st i in dom G holds f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X); set m = len G; A2: dom G = Seg m by FINSEQ_1:def 3; reconsider Z0 = 0.(product G) as Element of product carr G by Th10; reconsider x0 = x as Element of product carr G by Th10; reconsider x1 = x as (len G)-element FinSequence; reconsider Z1=0.(product G) as (len G)-element FinSequence; consider L be Lipschitzian LinearOperator of product G,S such that A3: for h be Point of product G ex w be FinSequence of S st dom w = Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).h)) & L.h = Sum w by Lm5; A4: for h be Point of product G ex w be FinSequence of S st dom w = dom G & (for i be set st i in dom G holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).h)) & L.h = Sum w proof let h be Point of product G; consider w be FinSequence of S such that A5: dom w = Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).h)) & L.h = Sum w by A3; take w; thus dom w = dom G by A5,FINSEQ_1:def 3; thus thesis by A5,A2; end; consider d0 be Real such that A6: d0 >0 and A7: {y where y is Element of product G: ||. y-x .|| < d0} c= X by A1,NDIFF_1:3; set N = {y where y is Element of product G: ||. y-x .|| < d0}; N c= the carrier of product G by A7,XBOOLE_1:1; then A8: N is Neighbourhood of x by A6,NFCONT_1:def 1; A9: 1 <= m by NAT_1:14; then m in dom G by A2; then f is_partial_differentiable_on X,m by A1; then X c= dom f; then A10:N c= dom f by A7; deffunc RF(Element of product G) = f/.(x+\$1) - f/.x - L.\$1; consider R be Function of the carrier of product G,the carrier of S such that A11:for h be Element of the carrier of product G holds R.h = RF(h) from FUNCT_2:sch 4; now let r0 be Real; assume A12: r0 > 0; set r1=r0/2; set r=r1/m; defpred DSQ[Nat, Real] means ex k be Element of NAT st \$1=k & 0 < \$2 & for q be Element of product G st q in X & ||. q-x .|| < \$2 holds ||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r; A13:for k0 be Nat st k0 in Seg m holds ex d be Element of REAL st DSQ[k0,d] proof let k0 be Nat; assume A14: k0 in Seg m; reconsider k = k0 as Element of NAT by ORDINAL1:def 12; f`partial|(X,k) is_continuous_on X by A2,A14,A1; then consider d be Real such that A15: 0 < d & for q be Point of product G st q in X & ||. q- x .|| < d holds ||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r by A12,A1,NFCONT_1:19; reconsider d as Element of REAL by XREAL_0:def 1; take d; for q be Point of product G st q in X & ||. q-x .|| < d holds ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r proof let q be Point of product G; assume A16:q in X & ||. q- x .|| < d; then A17: ||. (f`partial|(X,k))/.q - (f`partial|(X,k))/.x .|| < r by A15; A18: f is_partial_differentiable_on X,k by A1,A14,A2; then (f`partial|(X,k))/.q = partdiff(f,q,k) by A16,Def9; hence ||. partdiff(f,q,k)- partdiff(f,x,k) .|| < r by A17,A18,A1,Def9; end; hence ex k be Element of NAT st k0=k & 0 < d & for q be Element of product G st q in X & ||. q-x .|| < d holds ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A15; end; consider Dseq be FinSequence of REAL such that A19: dom Dseq = Seg m & for i be Nat st i in Seg m holds DSQ[i,Dseq.i] from FINSEQ_1:sch 5(A13); m in Seg m by A9; then reconsider rDseq = rng Dseq as non empty ext-real-membered set by A19,FUNCT_1:3; reconsider rDseq as left_end right_end non empty ext-real-membered set; A20:min rDseq in rng Dseq by XXREAL_2:def 7; reconsider d1 = min rDseq as Real; set d = min(d0,d1); A21: d <= d0 & d <= d1 by XXREAL_0:17; consider i1 be object such that A22: i1 in dom Dseq & d1 = Dseq.i1 by A20,FUNCT_1:def 3; reconsider i1 as Nat by A22; A23:ex k be Element of NAT st i1=k & 0 < Dseq.i1 & for q be Element of product G st q in X & ||. q-x .|| < Dseq.i1 holds ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A22; A24:now let q be Element of product G; assume ||. q-x .|| < d; then ||. q-x .|| < d0 by A21,XXREAL_0:2; then q in {y where y is Element of product G: ||. y-x .|| < d0}; hence q in X by A7; end; A25:now let q be Element of product G, i be Element of NAT; assume A26: ||. q-x .|| < d & i in Seg m; reconsider i0=i as Nat; consider k be Element of NAT such that A27: i0 = k & 0 < Dseq.i0 & for q be Element of product G st q in X & ||. q-x .|| < Dseq.i0 holds ||. partdiff(f,q,k) - partdiff(f,x,k) .|| < r by A19,A26; Dseq.i0 in rng Dseq by A19,A26,FUNCT_1:3; then d1 <= Dseq.i0 by XXREAL_2:def 7; then d <= Dseq.i0 by A21,XXREAL_0:2; then ||. q-x .|| < Dseq.i0 by A26,XXREAL_0:2; hence ||. partdiff(f,q,i) - partdiff(f,x,i) .|| < r by A24,A26,A27; end; take d; thus 0 < d by A6,A22,A23,XXREAL_0:21; thus for y be Point of product G st y <> 0.(product G) & ||.y.|| < d holds ||.y.||"* ||. R/.y .|| < r0 proof let y be Point of product G; assume A28: y <> 0.(product G) & ||. y .||< d; set z= R/.y; consider h be FinSequence of product G, g be FinSequence of S, Z,y0 be Element of product carr G such that A30: y0=y & Z = 0.(product G) & len h = len G + 1 & len g = len G & (for i be Nat st i in dom h holds h/.i = Z +* (y0| Seg (len G + 1-'i))) & (for i be Nat st i in dom g holds g/.i = f/.(x+h/.i) - f/.(x+h/.(i+1))) & (for i be Nat, hi be Point of product G st i in dom h & h/.i= hi holds ||. hi .|| <=||. y .||) & f /.(x+y) - f/.x = Sum g by Th45; consider w be FinSequence of S such that A31: dom w = Seg m & (for i be Element of NAT st i in Seg m holds w.i = partdiff(f,x,i).(proj(In(i,dom G)).y)) & L.y = Sum w by A3; A32: dom idseq m = Seg m & rng idseq m = Seg m; then A33: dom Rev idseq m = Seg m & rng Rev idseq m = Seg m by FINSEQ_5:57; then reconsider Ri=Rev idseq m as Function of Seg m,Seg m by FUNCT_2:1; Ri is one-to-one onto by A32,FINSEQ_5:57; then reconsider Ri=Rev idseq m as Permutation of dom w by A31; A34: len (idseq m) = m & len w = m by A31,A32,FINSEQ_1:def 3; dom (w * Ri) = dom Ri by A33,RELAT_1:27; then A35: dom (w * Ri) = dom Rev w by A33,A31,FINSEQ_5:57; reconsider wRi=w * Ri as FinSequence of S by FINSEQ_2:47; now let k be Nat; assume A36: k in dom Rev w; then A37: k in dom Rev idseq m by A33,A31,FINSEQ_5:57; then A38: 1 <= k & k <= m by A33,FINSEQ_1:1; then reconsider mk=m-k as Nat by NAT_1:21; reconsider zr0=0 as Nat; 0 <= mk; then A39: zr0 + 1 <= m - k + 1 by XREAL_1:6; k-1 >= 1-1 by A38,XREAL_1:9; then m-(k-1) <= m by XREAL_1:43; then A40: mk+1 in Seg m by A39; (Rev w).k = w.(len (idseq m) - k + 1) by A34,A36,FINSEQ_5:def 3 .= w.((idseq m).(len (idseq m) - k + 1)) by A40,A34,FINSEQ_2:49 .= w.((Rev idseq m).k) by A37,FINSEQ_5:def 3; hence (Rev w).k = wRi.k by A36,A35,FUNCT_1:12; end; then A41: Sum Rev w = Sum w by A35,FINSEQ_1:13,RLVECT_2:7; deffunc GW(Nat) = g/.\$1 - (Rev w)/.\$1; consider gw be FinSequence of S such that A42: len gw =m & for j being Nat st j in dom gw holds gw.j = GW(j) from FINSEQ_2:sch 1; A43: now let j be Nat; assume j in dom g; then j in Seg m by A30,FINSEQ_1:def 3; then j in dom gw by A42,FINSEQ_1:def 3; hence gw.j = g/.j - (Rev w)/.j by A42; end; len Rev w = len g by A30,A34,FINSEQ_5:def 3; then Sum gw = Sum g - Sum(Rev w) by A30,A42,A43,RLVECT_2:5; then A44: R/.y = Sum gw by A11,A30,A31,A41; A45: for j be Element of NAT st j in dom gw holds ||. gw/.j .|| <= ||. y .||*r proof let j be Element of NAT; assume A46: j in dom gw; then A47: j in Seg m by A42,FINSEQ_1:def 3; then A48: j in dom g by A30,FINSEQ_1:def 3; then A49: g/.j = f/.(x+h/.j) - f/.(x+h/.(j+1)) by A30; A50: 1 <= j & j <=m by A47,FINSEQ_1:1; then m+1 <= m+j & j+1 <= m+1 by XREAL_1:6; then m+1-j <= m & 1 <= m+1-j by XREAL_1:19,20; then m+1-'j <= m & 1 <= m+1-'j by A50,NAT_D:37; then A52: m+1-'j in Seg m; then f is_partial_differentiable_on X,(m+1-'j) by A1,A2; then A53: X c=dom f & for x be Element of product G st x in X holds f is_partial_differentiable_in x,(m+1-'j) by Th24,A1; w/.(m+1-'j) = w.(m+1-'j) by A31,A52,PARTFUN1:def 6; then A54: w/.(m+1-'j) = (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y) by A52,A31; A55: now let j be Element of NAT; reconsider hj = h/.j as Element of product G; assume 1 <= j & j <= m + 1; then A56: ||. hj .|| <= ||. y .|| by A30,FINSEQ_3:25; (x+h/.j)-x = h/.j + (x-x) by RLVECT_1:28 .= h/.j + 0.(product G) by RLVECT_1:15; then (x+h/.j)-x = h/.j by RLVECT_1:4; hence ||. (x+h/.j)-x .|| < d by A56,A28,XXREAL_0:2; end; Seg m c= Seg(m+1) by FINSEQ_1:5,NAT_1:11; then 1 <= j & j <= m + 1 by A47,FINSEQ_1:1; then A57: ||. (x+h/.j)-x .|| < d by A55; 1 <= j+1 by NAT_1:11; then A58: ||. (x+h/.(j+1))-x .|| < d by A50,A55,XREAL_1:6; A59: x + h/.j = reproj(In(m+1-'j,dom G),(x+h/.(j+1)) ) .(proj(In(m+1-'j,dom G)).(x+y)) by Th54,A30,A50; A60: (proj(In(m+1-'j,dom G)).(x+y)) - proj(In(m+1-'j,dom G)).(x+h/.(j+1)) = (proj(In(m+1-'j,dom G)).y) by Th55,A30,A50; for z be Point of product G st ||. z-x .|| < d holds ||. partdiff(f,z,(m+1-'j)) - partdiff(f,x,(m+1-'j)).|| <=r by A25,A52; then A61: ||. f/.(x+h/.j) - f/.(x+h/.(j+1)) - (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y).|| <= ||.(proj(In(m+1-'j,dom G)).y).|| *r by A1,A53,A52,A2,A24,A57,A58,A59,A60,Th53; A62: m+1-'j = m+1-j by A50,NAT_1:12,XREAL_1:233; j in Seg len (Rev w) by A42,A46,A34,FINSEQ_1:def 3,FINSEQ_5:def 3; then A63: j in dom Rev w by FINSEQ_1:def 3; then A64: (Rev w)/.j = (Rev w).j by PARTFUN1:def 6 .= w.(m-j+1) by A34,A63,FINSEQ_5:def 3 .= w/.(m+1-'j) by A62,A52,A31,PARTFUN1:def 6; A65: gw/.j = gw.j by A46,PARTFUN1:def 6 .= f/.(x+h/.j) - f/.(x+h/.(j+1)) - (partdiff(f,x,(m+1-'j))).(proj(In(m+1-'j,dom G)).y) by A54,A49,A64,A48,A43; ||. (proj(In(m+1-'j,dom G)).y).||*r <= ||. y .||*r by A12,Th31,XREAL_1:64; hence ||. gw/.j .|| <= ||. y .||*r by A65,A61,XXREAL_0:2; end; defpred YSQ[set,set] means \$2 = ||. gw/.\$1 .||; A66: for k be Nat st k in Seg m holds ex x be Element of REAL st YSQ[k,x]; consider yseq be FinSequence of REAL such that A67: dom yseq = Seg m & for i be Nat st i in Seg m holds YSQ[i,yseq.i] from FINSEQ_1:sch 5(A66); A68: len gw = len yseq by A42,A67,FINSEQ_1:def 3; A69: now let i be Element of NAT; assume i in dom gw; then i in Seg m by A42,FINSEQ_1:def 3; hence yseq.i = ||. gw/.i .|| by A67; end; reconsider yseq as Element of REAL m by A68,A42,FINSEQ_2:92; A70: ||. Sum gw .|| <= Sum yseq by A69,A68,Th7; reconsider yr = ||. y .||*r as Element of REAL by XREAL_0:def 1; for j be Nat st j in Seg m holds yseq.j <= (m |-> yr).j proof let j be Nat; assume A71: j in Seg m; then j in dom gw by A42,FINSEQ_1:def 3; then A72: ||. gw/.j .|| <= ||. y .||*r by A45; yseq.j = ||. gw/.j .|| by A67,A71; hence yseq.j <= (m |-> yr).j by A71,A72,FINSEQ_2:57; end; then Sum yseq <= Sum(m |-> yr) by RVSUM_1:82; then Sum yseq <= m*(||. y .||*r) by RVSUM_1:80; then ||. z .|| <= m*(||. y .||*r) by A44,A70,XXREAL_0:2; then ||. z .||*||.y.||" <= (m*||. y .||*r)*||.y.||" by XREAL_1:64; then ||. z .||*||.y.||" <= m*((r*||. y .||)*||.y.||"); then ||.y.||"* ||. z .|| <= m*r by A28,NORMSP_0:def 5,XCMPLX_1:203; then A73: ||.y.||"* ||. z .|| <= r1 by XCMPLX_1:87; r1 < r0 by A12,XREAL_1:216; hence (||.y.||"* ||. z .||) < r0 by A73,XXREAL_0:2; end; end; then reconsider R as RestFunc of product G,S by NDIFF_1:23; reconsider L as Point of R_NormSpace_of_BoundedLinearOperators(product G,S) by LOPBAN_1:def 9; A74: for y being Point of product G st y in N holds f/.y - f/.x = L.(y-x) + R/.(y-x) proof let y be Point of product G; assume y in N; y-x in the carrier of (product G); then y-x in dom R by PARTFUN1:def 2; then R/.(y-x) = R.(y-x) by PARTFUN1:def 6; then R/.(y-x) = f/.(x+(y-x)) - f/.x - L.(y-x) by A11; hence L.(y-x) + R/.(y-x) = f/.(x+(y-x)) - f/.x - (L.(y-x) - L.(y-x)) by RLVECT_1:29 .= f/.(x+(y-x)) - f/.x - 0.S by RLVECT_1:5 .= f/.(x+(y-x)) - f/.x by RLVECT_1:13 .= f/.(y-(x-x)) - f/.x by RLVECT_1:29 .= f/.(y-0.(product G)) - f/.x by RLVECT_1:5 .= f/.y - f/.x by RLVECT_1:13; end; then f is_differentiable_in x by A10,A8,NDIFF_1:def 6; then diff(f,x) = L by A8,A10,A74,NDIFF_1:def 7; hence thesis by A4,A74,A10,A8,NDIFF_1:def 6; end; theorem for G be RealNormSpace-Sequence, F be RealNormSpace, f be PartFunc of product G, F, X be Subset of product G st X is open holds (for i be set st i in dom G holds f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X) iff f is_differentiable_on X & f`|X is_continuous_on X proof let G be RealNormSpace-Sequence, F be RealNormSpace, f be PartFunc of product G, F, X be Subset of product G; assume A1: X is open; set m=len G; A2: dom G = Seg m by FINSEQ_1:def 3; hereby assume A3: for i be set st i in dom G holds f is_partial_differentiable_on X,i & f`partial|(X,i) is_continuous_on X; A4: now let i be Element of NAT; assume 1 <=i & i <= m; then i in Seg m; then f`partial|(X,i) is_continuous_on X by A3,A2; hence X c= dom (f`partial|(X,i)) & for y0 be Point of product G, r be Real st y0 in X & 0 0 by A12; let y1 be Point of product G; assume A14: y1 in X & ||. y1- y0 .|| < s; reconsider DD=diff(f,y1)-diff(f,y0) as Lipschitzian LinearOperator of product G, F by LOPBAN_1:def 9; A15: upper_bound PreNorms(DD) = ||. diff(f,y1) - diff(f,y0) .|| by LOPBAN_1:30; now let mt be Real; assume mt in PreNorms(DD); then consider t being VECTOR of product G such that A16: mt=||.DD.t.|| & ||.t.|| <= 1; consider w0 be FinSequence of F such that A17: dom w0 = dom G & (for i be set st i in dom G holds w0.i = partdiff(f,y0,i).(proj(In(i,dom G)).t)) & diff(f,y0).t=Sum(w0) by A1,A3,Th56,A9; reconsider Sw0=Sum w0 as Point of F; consider w1 be FinSequence of F such that A18: dom w1 = dom G & (for i be set st i in dom G holds w1.i = partdiff(f,y1,i).(proj(In(i,dom G)).t)) & diff(f,y1).t=Sum(w1) by A1,A3,Th56,A14; reconsider Sw1=Sum w1 as Point of F; deffunc F(set) = w1/.\$1 - w0/.\$1; consider w2 being FinSequence of F such that A19: len w2 = m & for i being Nat st i in dom w2 holds w2.i = F(i) from FINSEQ_2:sch 1; A20: len w1 = m & len w0 = m by A2,A17,A18,FINSEQ_1:def 3; now let i be Nat; assume i in dom w1; then i in dom w2 by A19,A2,A18,FINSEQ_1:def 3; hence w2.i = F(i) by A19; end; then Sum w2 = Sum w1 - Sum w0 by A19,A20,RLVECT_2:5; then A21: mt= ||. Sum w2 .|| by A16,A18,A17,LOPBAN_1:40; deffunc F(Nat) = In(||. (w2/.\$1) .||,REAL); consider ys being FinSequence of REAL such that A22: len ys = m & for j being Nat st j in dom ys holds ys.j = F(j) from FINSEQ_2:sch 1; A23: now let i be Element of NAT; assume i in dom w2; then i in Seg m by A19,FINSEQ_1:def 3; then i in dom ys by A22,FINSEQ_1:def 3; hence ys.i = F(i) by A22 .= ||.w2/.i.||; end; then A24: ||. Sum w2 .|| <= Sum ys by A19,A22,Th7; reconsider rm=r/(2*m) as Element of REAL by XREAL_0:def 1; deffunc F(Nat) = rm; consider rs being FinSequence of REAL such that A25: len rs = m & for j being Nat st j in dom rs holds rs.j = F(j) from FINSEQ_2:sch 1; A26: dom rs = Seg m by A25,FINSEQ_1:def 3; now let a be object; assume a in rng rs; then consider b being object such that A27: b in dom rs & a=rs.b by FUNCT_1:def 3; reconsider b as Nat by A27; rs.b=rm by A27,A25; hence a in {rm} by A27,TARSKI:def 1; end; then A28: rng rs c= {rm}; now let a be object; assume a in {rm}; then A29: a = rm by TARSKI:def 1; A30: 1 in dom rs by A5,A26; then a = rs.1 by A29,A25; hence a in rng rs by A30,FUNCT_1:3; end; then {rm} c= rng rs; then rs = m |-> (r/(2*m)) by A26,A28,XBOOLE_0:def 10,FUNCOP_1:9; then Sum rs = m*(r/(2*m)) by RVSUM_1:80 .= m*(r/2/m) by XCMPLX_1:78; then A31: Sum rs = r/2 by XCMPLX_1:87; now let i be Element of NAT; assume i in dom ys; then A32: i in Seg m by A22,FINSEQ_1:def 3; then A33: i in dom w2 & i in dom w1 & i in dom w0 by A17,A18,A19,FINSEQ_1:def 3; then A34: ys.i = ||. w2/.i .|| & w2/.i= w2.i by A23,PARTFUN1:def 6; A35: i in dom rs by A25,A32,FINSEQ_1:def 3; reconsider p1=partdiff(f,y1,i),p0 = partdiff(f,y0,i) as Lipschitzian LinearOperator of G.(In(i,dom G)), F by LOPBAN_1:def 9; reconsider P1 = p1.(proj(In(i,dom G)).t) as VECTOR of F; reconsider P0=p0.(proj(In(i,dom G)).t ) as VECTOR of F; w0/.i = w0.i & w1/.i = w1.i by A33,PARTFUN1:def 6; then w0/.i = P0 & w1/.i = P1 by A2,A17,A18,A32; then A36: w2.i = P1-P0 by A33,A19; 1 <= i & i <= len S by A13,A32,FINSEQ_1:1; then A37: s <= S.i & f is_partial_differentiable_on X,i by A2,A32,A3,RFINSEQ2:2; then ||. y1- y0 .|| < S.i by A14,XXREAL_0:2; then ||. (f`partial|(X,i))/.y1-(f`partial|(X,i))/.y0 .||