0 ex d be Real st d > 0 & for z be Real st z <> 0 & |. z .| < d holds |. z .|"* ||. R/.z .|| < r by A7,A17,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 convergent_to_0 Real_Sequence; A23: s is convergent & lim s = 0 by FDIFF_1:def 1; A24: now let r be Real; assume r > 0; then consider d be Real such that A25: d > 0 and A26: for z be Real st z <> 0 & |.z.| < d holds |.z.|"* ||. R/.z .|| < r by A21; consider n0 be Element of NAT such that A27: for m be Element of NAT st n0 <=m holds |. s.m-0 .| < d by A23,A25,SEQ_2:def 7; take n0; thus for m be Element of NAT st n0 <=m holds ||. ((s")(#)(R/*s)).m- 0.S .|| < r proof A28: rng s c= dom R by A1; let m be Element of NAT; assume n0 <=m; then B29: |. s.m-0 .| < d by A27; s is non-zero by FDIFF_1:def 1; then A30: s.m <> 0 by SEQ_1:5; |. s.m .|" * ||. R/.(s.m) .|| = abs((s.m)") * ||. R/.(s.m) .|| by COMPLEX1:66 .= ||. (s.m)"*(R/.(s.m)) .|| by NORMSP_1:def 1 .= ||. (s.m)"*((R/*s).m) .|| by A28,FUNCT_2:109 .= ||. (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 A26,B29,A30; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.S by A24,NORMSP_1:def 7; end; hence R is REST-like by NDIFF_3:def 1; end; hence thesis by A2; end; theorem NDIFF27: for R be REST 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 REST 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,NDIFF126; take d; now let h be Real such that A5: |.h.| < d; B1: 0 <= |.h.| by COMPLEX1:46; per cases; suppose A6: h <> 0; then |.h.|"*||. R/.h .|| <= e by A4,A5; then |.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by B1,XREAL_1:64; then A7: |.h.|*|.h.|"*||. R/.h .|| <= e * |.h.|; |.h.| <> 0 by A6,COMPLEX1:45; then 1*||. R/.h .|| <= e * |.h.| by A7,XCMPLX_0:def 7; hence ||. R/.h .|| <= e* |.h.|; end; suppose A8: h = 0; reconsider p0=0 as Real; p0* |.h.| <= e* |.h.| by A2,B1; hence ||. R/.h .|| <= e* |.h.| by A1,A8; end; end; hence thesis by A3; end; theorem NDIFF29: for R be REST of S for L be Lipschitzian LinearOperator of S,T holds L*R is REST of T proof let R be REST 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 A8: e > 0; set e1 = e/2/(1 + K); consider d be Real such that A10: 0 < d and A11: for h be Real st h <> 0 & |.h.| < d holds |.h.|"* ||. R/.h .|| < e1 by A1,A4,A8,NDIFF126; A12: e/2 < e by A8,XREAL_1:216; now let h be Real; assume A13: h <> 0 & |.h.| < d; then |.h.|"* ||.(R/.h).|| < e1 by A11; then (K +1)*(|.h.|"* ||.R/.h.||) <= (K +1)*e1 by A1,XREAL_1:64; then A15: (K +1)*(|.h.|"* ||.R/.h.||) <= e/2 by A1,XCMPLX_1:87; |.h.| <> 0 by A13,COMPLEX1:45; then A16: |.h.| > 0 by COMPLEX1:46; reconsider p0=0, p1=1 as Real; p0 + K < p1 + K by XREAL_1:8; then A17: 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 A17,XXREAL_0:2; then |.h.|"* ||.L.(R/.h).|| <= |.h.|"*((K +1)*||. R/.h .||) by A16,XREAL_1:64 ; then A18: |.h.|"* ||.L.(R/.h).|| <= e/2 by A15,XXREAL_0:2; L.(R/.h) = L/.(R/.h); then L.(R/.h) =(L*R)/.h by A5,A3,PARTFUN2:5; hence |.h.|"* ||.(L*R)/.h.|| < e by A12,A18,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 A10; end; hence thesis by A4,NDIFF126; end; theorem NDIFF211: for R1 be REST of S st R1/.0 = 0.S for R2 be REST of S,T st R2/.(0.S) = 0.T for L be LINEAR of S holds R2*(L+R1) is REST of T proof let R1 be REST 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 NDIFF27; let R2 be REST of S,T such that A3:R2/.(0.S) = 0.T; let L be LINEAR 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 A6:rng(L+R1) c= dom R2; R1 is total by NDIFF_3:def 1; then L+R1 is total by VFUNCT_1:32; then A8:dom(L+R1) = REAL by PARTFUN1:def 2; then dom(R2*(L+R1)) = REAL by A6,RELAT_1:27; then A9:R2*(L+R1) is total by PARTFUN1:def 2; now let e be Real such that A10: e > 0; A11: e/2 < e by A10,XREAL_1:216; set e1 = e/2/(1 + K); consider d be Real such that A12: 0 < d and A13: for z be Point of S st ||.z.|| < d holds ||.R2/.z.|| <= e1*||.z.|| by A3,A10,NDIFF_2:7; set d1 = d/(1 + K); set dd1 = min(d0,d1); A14: dd1 <= d1 & dd1 <= d0 by XXREAL_0:17; A16: now let h be Real such that A17: h <> 0 and A18: |.h.| < dd1; |.h.| < d0 by A14,A18,XXREAL_0:2; then A19: ||.R1/.h.|| <=1* |.h.| by A2; reconsider p0=0 as Real; 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 A19,NORMSP_1:def 1,XREAL_1:7; then A20: ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2; then A21: e1 * ||. L.h+R1/.h .|| <= e1*((K +1)*|.h.|) by A10,XREAL_1:64; |.h.| < d1 by A14,A18,XXREAL_0:2; then (K +1) * |.h.| < (K +1) * d1 by XREAL_1:68; then ||. L.h+R1/.h .|| < (K +1) * d1 by A20,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 A13; then A22: ||. R2/.(L.h+R1/.h) .|| <= e1*((K +1)*|.h.|) by A21,XXREAL_0:2; A23: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h) .=R2/.((L+R1)/.h) by A8,VFUNCT_1:def 1 .=(R2*(L+R1))/.h by A8,A6,PARTFUN2:5; A24: |.h.| <> 0 by A17,COMPLEX1:45; then |.h.| > 0 by COMPLEX1:46; then |.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* (K +1) * |.h.|) by A23,A22,XREAL_1:64; then |.h.|"* ||. (R2*(L+R1))/.h .|| <= |.h.|*|.h.|"*e1*(K +1); then |.h.|"* ||. (R2*(L+R1))/.h .|| <= 1 * e1 * (K +1) by A24,XCMPLX_0:def 7; then |.h.|"* ||. (R2*(L+R1))/.h .|| <= e/2 by XCMPLX_1:87; hence |.h.|"* ||.(R2*(L+R1))/.h.|| < e by A11,XXREAL_0:2; end; 0 < dd1 by A1,A12,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 A16; end; hence thesis by A9,NDIFF126; end; theorem NDIFF212: for R1 be REST of S st R1/.0=0.S for R2 be REST of S,T st R2/.(0.S)=0.T for L1 be LINEAR of S for L2 be Lipschitzian LinearOperator of S,T holds L2*R1 + R2*(L1+R1) is REST of T proof let R1 be REST of S such that A1: R1/.0=0.S; let R2 be REST of S,T such that A2: R2/.(0.S)=0.T; let L1 be LINEAR of S; let L2 be Lipschitzian LinearOperator of S,T; L2*R1 is REST of T & R2*(L1+R1) is REST of T by A1,A2,NDIFF211,NDIFF29; hence thesis by NDIFF_3:7; end; theorem NDIFF213: for x0 be Element of 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 Element of 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 LINEAR of S,R1 be REST 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 REST 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 REST 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 LINEAR of S,R1 be REST of S such that A9: 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 B9: for p be Real holds L1.p = p*r by NDIFF_3:def 2; reconsider p0=0 as Element of REAL; g/.x0-g/.x0 = L1.(x0-x0) + R1/.(x0-x0) by A9,RCOMP_1:16; then 0.S = L1.0 + R1/.0 by RLVECT_1:15; then 0.S = p0*r + R1/.0 by B9; 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 REST of T by A6,NDIFF212; B11: dom(L2*L1) = REAL by FUNCT_2:def 1; reconsider q = L2.r as Point of T; now let p be Real; L2.(L1.p) = L2.(p*r) by B9; then L2.(L1.p) = p*q by LOPBAN_1:def 5; hence (L2*L1).p = p*q by B11,FUNCT_1:12; end; then reconsider L0=L2*L1 as LINEAR 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 A10: g.:N3 c= N2 by NFCONT_3:10; consider N be Neighbourhood of x0 such that A11: N c= N1 and A12: N c= N3 by RCOMP_1:17; now let x be set; assume A14: x in N; then reconsider x9 = x as Real; A15: x in N1 by A11,A14; then g.x9 in g.:N3 by A2,A12,A14,FUNCT_1:def 6; then g.x9 in N2 by A10; hence x in dom(f*g) by A2,A4,A15,FUNCT_1:11; end; then A13: N c= dom(f*g) by TARSKI:def 3; A17: now let x be Real such that A18: x in N; A19: g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A9,A11,A18; A20: x in N1 by A11,A18; then g.x in g.:N3 by A2,A12,A18,FUNCT_1:def 6; then g.x in N2 by A10; then A21: g/.x in N2 by A2,A20,PARTFUN1:def 6; A23: x0 in N by RCOMP_1:16; A24: R1 is total by NDIFF_3:def 1; then A25: dom R1 = REAL by PARTFUN1:def 2; dom L2 = the carrier of S by FUNCT_2:def 1; then A26: rng R1 c= dom L2; A27: dom(L2*R1) = REAL by A24,PARTFUN1:def 2; L1+R1 is total by A24,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 A27,A29,VFUNCT_1:def 1; L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0)); then A32: L2.(R1/.(x-x0)) =(L2*R1)/.(x-x0) by A25,A26,PARTFUN2:5; A33: R2/.(L1.(x-x0)+R1/.(x-x0)) = R2/.(L1/.(x-x0)+R1/.(x-x0)) .=R2/.((L1+R1)/.(x-x0)) by A29,VFUNCT_1:def 1 .=(R2*(L1+R1))/.(x-x0) by A29,A30,PARTFUN2:5; B33: (L2*L1).(x-x0) = L2.(L1.(x-x0)) by B11,FUNCT_1:12; thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A13,A18,PARTFUN2:3 .=f/.(g/.x) -f/.(g/.x0) by A13,A23,PARTFUN2:3 .=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A21 .=L2.(L1.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A19,A33, GRCAT_1:def 8 .=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 B33,A31,VFUNCT_1:def 1; end; hence A34: f*g is_differentiable_in x0 by A13,NDIFF_3:def 3; (L2*L1).1 = diff(f,g/.x0).diff(g,x0) by A9,B11,FUNCT_1:12; hence thesis by A34,A13,A17,NDIFF_3:def 4; end; theorem PDIFF617: 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 B1: 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 Function of NAT,the carrier of S such that B3: Sum xseq = Sx.(len xseq) & Sx.0 = 0.S & for j be Element of 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 B1; hence thesis by B1,B3,RVSUM_1:72; end; A4:now let i be Element of NAT; assume A4: P[i]; now let xseq be FinSequence of S, yseq be FinSequence of REAL; set xseq0=xseq|i, yseq0=yseq|i; assume A5: i+1=len xseq & len xseq = len yseq & ( for i be Element of NAT st i in dom xseq holds yseq.i = ||. xseq/.i .|| ); A6: for k be Element of NAT st k in dom xseq0 holds yseq0.k = ||. xseq0/.k .|| proof let k be Element of NAT; assume A9: k in dom xseq0; then A7: k in Seg i & k in dom xseq by RELAT_1:57; then A8: yseq.k = ||. xseq/.k .|| by A5; xseq/.k = xseq.k by A7,PARTFUN1:def 6; then xseq/.k = xseq0.k by A7,FUNCT_1:49; then xseq/.k = xseq0/.k by A9,PARTFUN1:def 6; hence thesis by A7,A8,FUNCT_1:49; end; C1: dom xseq = Seg(i+1) by A5,FINSEQ_1:def 3; then A9: yseq.(i+1) = ||. xseq/.(i+1) .|| by A5,FINSEQ_1:4; A10: 1 <= i + 1 by NAT_1:11; yseq = (yseq|i)^<*yseq/.(i+1) *> by A5,FINSEQ_5:21; then yseq = yseq0 ^<*(yseq.(i+1))*> by A5,A10,FINSEQ_4:15; then A11: Sum yseq = Sum yseq0 + yseq.(i+1) by RVSUM_1:74; B1: len xseq in dom xseq by C1,A5,FINSEQ_1:4; then reconsider v = xseq.(len xseq) as Element of S by PARTFUN1:4; B2: v = xseq/.(i+1) by A5,B1,PARTFUN1:def 6; A12: i=len xseq0 by A5,FINSEQ_1:59,NAT_1:11; then xseq0 = xseq| (dom xseq0) by FINSEQ_1:def 3; then A13: Sum xseq = Sum xseq0 + v by A5,A12,RLVECT_1:38; A14: ||. Sum xseq0 + v.|| <= ||.Sum xseq0 .|| + ||. v .|| by NORMSP_1:def 1; len xseq0 = len yseq0 by A5,A12,FINSEQ_1:59,NAT_1:11; then ||. Sum xseq0 .|| <= Sum yseq0 by A4,A6,A12; then ||. Sum xseq0 .|| + ||.v.|| <= Sum yseq0 + yseq.(i+1) by A9,B2,XREAL_1:6; hence ||. Sum xseq .|| <= Sum yseq by A11,A13,A14,XXREAL_0:2; end; hence P[i+1]; end; for i be Element of NAT holds P[i] from NAT_1:sch 1(A3,A4); hence thesis by A1,A2; end; theorem Lm1: 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,XBOOLE_1:1; hence thesis by A3,NFCONT_1:def 1; end; theorem LMPROD1: 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 X1: x = g & dom g = dom X & for i be set st i in dom X holds g.i in X.i by CARD_3:def 5; dom g = Seg len X by X1,FINSEQ_1:def 3; hence x is FinSequence by X1,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 LMPROD1; end; end; ZE: 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 LMPROD1; dom carr G = dom G by ZE; then zz.j in carr G.j by CARD_3:9; hence thesis by PRVECT_2:def 4; end; end; theorem LM001: 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 LM003: 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 AS: r in the carrier of (G.i) & x in product carr G; then consider g be Function such that P1: x = g & dom g = dom carr G & for i be set 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 X2:dom s = {i} by FUNCOP_1:13; P2:dom h = dom carr G by P1,FUNCT_7:30; for j be set st j in dom carr G holds h.j in (carr G).j proof let j be set; assume A0: j in dom carr G; per cases; suppose not j in dom s; then j <> i by X2,TARSKI:def 1; then h.j = x.j by FUNCT_7:32; hence h.j in (carr G).j by P1,A0; end; suppose j in dom s; then X4: j = i by X2,TARSKI:def 1; then h.j = r by A0,P1,FUNCT_7:31; hence h.j in (carr G).j by AS,X4,PRVECT_2:def 4; end; end; then x +* (i,r) in product carr G by P2,CARD_3:def 5; hence thesis by LM001; end; definition let G be RealNormSpace-Sequence; attr G is non-trivial means :defTRV: 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 defTRV; end; registration let G be non-trivial RealNormSpace-Sequence; cluster product G -> non trivial; correctness proof X1:the carrier of product G = product carr G by LM001; not for x,y be set st x in product carr G & y in product carr G holds x = y proof assume A0: for x,y be set st x in product carr G & y in product carr G holds x = y; consider z be set such that P0: z in product carr G by XBOOLE_0:def 1; consider g be Function such that P1: z = g & dom g = dom carr G & for i be set st i in dom carr G holds g.i in (carr G).i by P0,CARD_3:def 5; set i = the Element of dom G; now let r,s be set; assume P2: 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 LM003,P0,P1,P2; then g +* (i,r) in product carr G & g +* (i,s) in product carr G by LM001; then KK: g +* (i,r) = g +* (i,s) by A0; i in dom G; then F1: i in dom g by P1,ZE; then (g +* (i,r)).i = r by FUNCT_7:31; hence r=s by KK,F1,FUNCT_7:31; end; hence contradiction by ZFMISC_1:def 10; end; hence thesis by X1,ZFMISC_1:def 10; end; end; theorem ADD1: 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 AS0: p=p0 & q=q0; len carr G = len G by PRVECT_2:def 4; then B1:dom carr G = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; P1: product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop G:], productnorm G #) by PRVECT_2:6; hereby assume AS1: p+q = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by B1; (addop G).i0 = the addF of (G.i0) by PRVECT_2:def 5; hence r0.i = p0.i + q0.i by AS0,AS1,P1,PRVECT_1:def 8; end; end; assume AS: 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 LM001; X1:ex g be Function st pq = g & dom g = dom carr G & for i be set st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; X2:ex g be Function st r0 = g & dom g = dom carr G & for i be set st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be set; assume AS1: i0 in dom pq; then reconsider i1=i0 as Element of dom G by B1,X1; reconsider i =i0 as Element of dom carr G by AS1,X1; (addop G).i = the addF of (G.i) by PRVECT_2:def 5; then pq.i0 = p0.i1 + q0.i1 by AS0,P1,PRVECT_1:def 8; hence pq.i0 = r0.i0 by AS; end; hence p+q = r0 by X1,X2,FUNCT_1:2; end; theorem MLT1: 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 AS0: p=p0; hereby assume AS1: r*p = r0; hereby let i be Element of dom G; reconsider i0=i as Element of dom carr G by ZE; X1: (multop G).i0 = the Mult of (G.i0) by PRVECT_2:def 8; product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; hence r0.i = r*(p0.i) by AS0,AS1,X1,PRVECT_2:def 2; end; end; assume AS2: for i be Element of dom G holds r0.i = r* (p0.i); reconsider rp = r*p as Element of product carr G by LM001; X1:ex g be Function st rp = g & dom g = dom carr G & for i be set st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; X2:ex g be Function st r0 = g & dom g = dom carr G & for i be set st i in dom carr G holds g.i in (carr G).i by CARD_3:def 5; now let i0 be set; assume AS1: i0 in dom rp; then reconsider i1=i0 as Element of dom G by ZE,X1; reconsider i=i0 as Element of dom carr G by AS1,X1; P1: product G = NORMSTR(# product carr G,zeros G,[:addop G:], [:multop G:], productnorm G #) by PRVECT_2:6; (multop G).i = the Mult of (G.i) by PRVECT_2:def 8; then rp.i0 = r*(p0.i1) by AS0,P1,PRVECT_2:def 2; hence rp.i0 = r0.i0 by AS2; end; hence r*p = r0 by X1,X2,FUNCT_1:2; end; theorem ZR1: 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; B1:dom carr G = dom G by ZE; P1: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 B1,PRVECT_2:def 7; assume AS1: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 ZE; p0.i0 = 0.(G.i) by AS1; hence p0.i0 = the ZeroF of (G.i0); end; hence 0.(product G)=p0 by P1,PRVECT_2:def 7; end; theorem SUB1: 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 AS0: p=p0 & q=q0; reconsider qq0=(-1)*q as Element of product carr G by LM001; X0:p-q = p+(-1)*q by RLVECT_1:16; hereby assume AS1: 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; X1: r0.i = p0.i + qq0.i by ADD1,AS1,AS0,X0; -1 is Real by XREAL_0:def 1; then qq0.i = (-1)*(q0.i) by AS0,MLT1; hence thesis by X1,RLVECT_1:16; end; end; assume AS2: for i be Element of dom G holds r0.i = p0.i - q0.i; now let i be Element of dom G; -1 is Real by XREAL_0:def 1; then X2: qq0.i = (-1)*(q0.i) by AS0,MLT1; r0.i = p0.i - q0.i by AS2; hence r0.i = p0.i + qq0.i by X2,RLVECT_1:16; end; hence p-q = r0 by X0,ADD1,AS0; end; begin :: Mean value theorem for vector-valued functions definition let S be RealLinearSpace; let p,q be Point of S; func ]. p,q .[ -> Subset of S equals { p+t*(q-p) where t is Real : 0 < t & t < 1}; correctness proof now let x be set; assume x in { p+t*(q-p) where t is Real : 0 < t & t < 1}; then ex t be Real st x=p+t*(q-p) & 0 < t & t < 1; hence x in the carrier of S; end; hence thesis by TARSKI:def 3; end; end; notation let S be RealLinearSpace; let p,q be Point of S; synonym [.p,q.] for LSeg(p,q); end; LmX: 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; theorem LMDefCLS1: for S be RealLinearSpace, p,q be Point of S holds ].p,q.[ c= [. p,q .] proof let S be RealLinearSpace, p,q be Point of S; now let z be set; assume z in ].p,q.[; then consider z1 be Real such that AA: z=p+z1*(q-p) & 0 < z1 & z1 < 1; z = (1-z1)*p + z1*q by AA,LmX; then z in {(1-r)*p + r*q where r is Real : 0 <= r & r <= 1 } by AA; hence z in [. p,q .] by RLTOPSP1:def 2; end; hence ].p,q.[ c= [. p,q .] by TARSKI:def 3; end; LMFDAF10A: 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 NDIFF126A: for T be non trivial RealNormSpace, R be PartFunc of REAL,T st R is total holds R is REST-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & abs z < d holds ( ||. R/.z .||/ abs z ) < r proof let T be non trivial RealNormSpace, R be PartFunc of REAL,T; assume A1: R is total; A2:now assume A3: R is REST-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & abs z < d holds ( ||. R/.z .||/ abs 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 & abs z < d & not ( ||. R/.z .||/ abs z ) < r; defpred P[Element of NAT,Element of REAL] means $2 <> 0 & abs($2) < (1/($1+1)) & not ( (||. R/.$2 .||/abs($2) ) < r ); A6: now let n be Element of NAT; 1/(n + 1) is Real by XREAL_0:def 1; hence ex z be Element of REAL st P[n,z] by A5; 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(A6); A8: now let p be real number; assume A9: 0

0 ex d be Real st d > 0 & for z be Real st z <> 0 & abs z < d holds ( ||. R/.z .||/abs z ) < r by A7,A17,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 & abs(z) < d holds ( ||. R/.z .||/abs z) < r; now let s be convergent_to_0 Real_Sequence; A22: s is non-zero by FDIFF_1:def 1; A23: s is convergent & lim s = 0 by FDIFF_1:def 1; A24: now let r be Real; assume r > 0; then consider d be Real such that A25: d > 0 and A26: for z be Real st z <> 0 & abs z < d holds ( ||. R/.z .||/abs z) < r by A21; consider n be Element of NAT such that A27: for m be Element of NAT st n <=m holds abs(s.m-0) < d by A23,A25,SEQ_2:def 7; take n; thus for m be Element of NAT st n <=m holds ||. ((s")(#)(R/*s)).m- 0.T.|| < r proof dom R = REAL by A1,PARTFUN1:def 2; then A28: rng s c= dom R; let m be Element of NAT; assume n <=m; then A29: abs(s.m-0) < d by A27; A30: s.m <> 0 by A22,SEQ_1:5; ||.(R/.(s.m)).|| / abs(s.m) = abs((s.m)") * ||.(R/.(s.m)).|| by COMPLEX1:66 .= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1 .= ||.(s.m)"*((R/*s).m).|| by A28,FUNCT_2:109 .= ||.(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 A26,A29,A30; end; end; hence (s")(#)(R/*s) is convergent by NORMSP_1:def 6; hence lim ((s")(#)(R/*s)) = 0.T by A24,NORMSP_1:def 7; end; hence R is REST-like by A1,NDIFF_3:def 1; end; hence thesis by A2; end; theorem NDIFF126B: for R be Function of REAL,REAL holds R is REST-like iff for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & abs(z) < d holds (abs(R.z)/ abs(z)) < r proof let R be Function of REAL,REAL; A2:now assume A3: R is REST-like; assume not (for r be Real st r > 0 ex d be Real st d > 0 & for z be Real st z <> 0 & abs z < d holds ( abs(R.z)/ abs 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 & abs z < d & not ( abs(R.z)/abs z) < r; defpred P[Element of NAT,Element of REAL] means $2 <> 0 & abs $2 < 1/($1+1) & not (abs(R.$2)/abs $2) < r; A6: now let n be Element of NAT; 1/(n + 1) is Real by XREAL_0:def 1; hence ex z be Element of REAL st P[n,z] by A5; 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(A6); A8: now let p be real number; assume A9: 0

0 ex d be Real st d > 0 & for z be Real st
z <> 0 & abs z < d holds ( abs(R.z)/abs z ) < r by A7,A17,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 & abs z < d holds ( abs(R.z)/abs z ) < r;
now let s be convergent_to_0 Real_Sequence;
A22: s is non-zero by FDIFF_1:def 1;
A23: s is convergent & lim s = 0 by FDIFF_1:def 1;
A24: now let r be real number;
assume D1: r > 0;
r is Real by XREAL_0:def 1; then
consider d be Real such that
A25: d > 0 and
A26: for z be Real st z <> 0 & abs z < d holds abs(R.z)/abs z < r by D1,A21;
consider n be Element of NAT such that
A27: for m be Element of NAT st n <= m holds abs(s.m-0) < d
by A23,A25,SEQ_2:def 7;
take n;
hereby let m be Element of NAT;
assume n <=m; then
A29: abs(s.m-0) < d by A27;
A30: s.m <> 0 by A22,SEQ_1:5;
abs(R.(s.m)) / abs(s.m)
= abs((s.m)") * abs(R.(s.m)) by COMPLEX1:66
.= abs((s.m)" * R.(s.m)) by COMPLEX1:65
.= abs((s.m)" * (R/*s).m) by FUNCT_2:115
.= abs(s".m * (R/*s).m) by VALUED_1:10
.= abs((s"(#)(R/*s)).m - 0) by SEQ_1:8;
hence abs( ((s")(#)(R/*s)).m- 0) < r by A26,A29,A30;
end;
end;
hence (s")(#)(R/*s) is convergent by SEQ_2:def 6;
hence lim((s")(#)(R/*s)) = 0 by A24,SEQ_2:def 7;
end;
hence R is REST-like by FDIFF_1:def 2;
end;
hence thesis by A2;
end;
LMFDAF10:
for T be non trivial 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 number 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 non trivial 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 number st x in ].0,1.[ holds
||. diff(f,x) .|| <= diff(g,x));
now let e be Real;
assume P1: 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 set;
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 number;
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
P10: ex t be Real st r = t & 0<=t & t<=1; then
abs r = r by ABSVALUE:def 1;
hence abs r < 2 by P10,XXREAL_0:2;
end; then
Q1: B is real-bounded by SEQ_4:4;
set s = upper_bound B;
Q2: ex d be real number st 0 < d & d in B
proof
0 in [.0,1.]; then
consider d1 be real number such that
Q21: 0 < d1 & for x1 be real number st x1 in [.0,1.] & abs(x1-0) < d1
holds ||. f/.x1 - f/.0 .|| < e1 by P1,A1,NFCONT_3:17;
set d2=d1/2;
Q23: d2 < d1 by Q21,XREAL_1:216;
take d = min(d2,1);
thus Q26: 0 < d by Q21,XXREAL_0:21;
Q24: d <= 1 by XXREAL_0:17; then
Q27: d in [.0,1.] by Q26;
V24: d <= d2 by XXREAL_0:17;
abs(d-0) = d by Q26,ABSVALUE:def 1; then
abs(d-0) < d1 by V24,Q23,XXREAL_0:2; then
Q28: ||. f/.d - f/.0 .|| < e1 by Q21,Q27;
Q35: [.0,d.] c= dom g by A1,Q24,XXREAL_1:34;
Q30: g| [.0,d.] is continuous by A1,Q24,FCONT_1:16,XXREAL_1:34;
Q31: ].0,d.[ c=].0,1.[ by Q24,XXREAL_1:46; then
consider x0 be Real such that
Q33: x0 in ].0,d.[
& diff(g,x0) =(g.d-g.0)/(d-0) by A1,Q26,Q35,Q30,FDIFF_1:26,ROLLE:3;
||. diff(f,x0) .|| <= diff(g,x0) by A1,Q33,Q31; then
0 <= g.d-g.0 by Q26,Q33; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1
by Q28,XREAL_1:7; then
(0 qua Real) + ||. f/.d - f/.0 .|| <= (g.d - g.0) + e1+ e1*d
by Q26,P1,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 Q27;
end; then
Q3: 0 < s by Q1,SEQ_4:def 1;
now let r be real number;
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
Q4: s <= 1 by Q2,SEQ_4:45;
defpred P[Element of NAT,Element of REAL]
means $2 in B & abs(s-$2) <= 1/($1+1);
WQ0:now let x be Element of NAT;
reconsider t = 1/(1+x) as real number;
consider r be real number such that
WQ3: r in B & s-t < r by Q1,Q2,SEQ_4:def 1;
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
s-t + t < r + t by WQ3,XREAL_1:8; then
WQ4: s -r < t+r -r by XREAL_1:14;
r <= s by Q1,WQ3,SEQ_4:def 1; then
0 <= s - r by XREAL_1:48;
hence P[x,r] by WQ3,WQ4,SEQ_2:1;
end;
consider sq be Function of NAT,REAL such that
WQ1: for x being Element of NAT holds P[x, sq.x] from FUNCT_2:sch 10(WQ0);
reconsider sq as Real_Sequence;
XX: now let p1 be real number;
assume AS: 0 < p1;
set p = p1/2;
consider n be Element of NAT such that
U10: 1/p < n by SEQ_4:3;
1/p + (0 qua Real) < n+1 by U10,XREAL_1:8; then
U1: 1/(n+1) <= 1/(1/p) by AS,XREAL_1:118;
take n;
thus for m be Element of NAT st n<=m holds abs (sq.m-s) < p1
proof
let m be Element of 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
U3: 1/(m+1) <= p by U1,XXREAL_0:2;
sq.m in B & abs(s-sq.m) <= 1/(m+1) by WQ1; then
abs(sq.m-s) <= 1/(1+m) by COMPLEX1:60; then
U4: abs(sq.m-s) <= p by U3,XXREAL_0:2;
p < p1 by AS,XREAL_1:216;
hence thesis by U4,XXREAL_0:2;
end;
end; then
WQ2:sq is convergent by SEQ_2:def 6; then
WQ2A:lim sq = s by XX,SEQ_2:def 7;
deffunc F(Real) = ||. f/.$1 -f/.0 .|| - (g.$1 - g.0) - e1*$1 - e1;
WQ3:for x being Element of REAL holds F(x) in REAL;
consider Lg0 be Function of REAL,REAL such that
WQ4: for x being Element of REAL holds Lg0.x = F(x) from FUNCT_2:sch 8(WQ3);
set Lg = Lg0| [.0,1.];
W5: dom Lg0 = REAL by FUNCT_2:def 1; then
WQ50A:
dom Lg = [.0,1.] by RELAT_1:62;
now let y be set;
assume y in rng sq; then
ex x be set st x in NAT & sq.x = y by FUNCT_2:11; then
y in B by WQ1; 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
WQ50:
rng sq c= dom Lg by WQ50A,TARSKI:def 3;
AQ2:s in [.0,1.] by Q4,Q3;
now let r be real number;
set r3=r/3;
assume AQ10: 0