### The Mizar article:

### Functional Sequence from a Domain to a Domain

**by****Beata Perkowska**

- Received May 22, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: SEQFUNC
- [ MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, PARTFUN1, BOOLE, SEQ_1, FINSEQ_1, ARYTM_1, ABSVALUE, ARYTM_3, TDGROUP, SEQ_2, ORDINAL2, FCONT_1, SQUARE_1, SEQFUNC, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_1, ABSVALUE, SEQ_1, SEQ_2, FCONT_1, LIMFUNC1; constructors REAL_1, PARTFUN1, RFUNCT_1, ABSVALUE, SEQ_2, FCONT_1, LIMFUNC1, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, SEQ_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0; theorems FUNCT_1, PARTFUN1, REAL_1, TARSKI, ABSVALUE, RFUNCT_1, SEQ_1, SEQ_2, SEQ_4, ZFMISC_1, RFUNCT_2, SQUARE_1, FCONT_1, AXIOMS, FUNCT_2, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FUNCT_1, SEQ_1; begin reserve D,D1,D2 for non empty set, x,y,z for set, n,k for Nat, p,x1,r for Real, f for Function; definition let D1,D2; mode Functional_Sequence of D1,D2 -> Function means :Def1: dom it = NAT & rng it c= PFuncs(D1,D2); existence proof deffunc U(set) = {}; consider f be Function such that A1: dom f = NAT & for x st x in NAT holds f.x = U(x) from Lambda; take f; thus dom f = NAT by A1; let x; assume x in rng f; then ex y st y in dom f & f.y = x by FUNCT_1:def 5; then x = {} by A1; then x is PartFunc of D1,D2 by PARTFUN1:56; hence x in PFuncs(D1,D2) by PARTFUN1:119; end; end; reserve F,F1,F2 for Functional_Sequence of D1,D2; definition let D1,D2,F,n; redefine func F.n -> PartFunc of D1,D2; coherence proof n in NAT; then n in dom F by Def1; then A1: F.n in rng F by FUNCT_1:def 5 ; rng F c= PFuncs(D1,D2) by Def1; hence thesis by A1,PARTFUN1:120; end; end; reserve G,H,H1,H2,J for Functional_Sequence of D,REAL; Lm1: f is Functional_Sequence of D1,D2 iff (dom f = NAT & for x st x in NAT holds f.x is PartFunc of D1,D2) proof thus f is Functional_Sequence of D1,D2 implies (dom f=NAT & for x st x in NAT holds f.x is PartFunc of D1,D2) proof assume A1: f is Functional_Sequence of D1,D2; hence dom f=NAT by Def1; A2: rng f c=PFuncs(D1,D2) by A1,Def1; let x; assume x in NAT; then x in dom f by A1,Def1; then f.x in rng f by FUNCT_1:def 5; hence f.x is PartFunc of D1,D2 by A2,PARTFUN1:120; end; assume that A3: dom f= NAT and A4: for x st x in NAT holds f.x is PartFunc of D1,D2; now let y; assume y in rng f; then consider x such that A5: x in dom f and A6: y=f.x by FUNCT_1:def 5; f.x is PartFunc of D1,D2 by A3,A4,A5; hence y in PFuncs(D1,D2) by A6,PARTFUN1:119; end; then rng f c=PFuncs(D1,D2) by TARSKI:def 3; hence thesis by A3,Def1; end; theorem f is Functional_Sequence of D1,D2 iff (dom f = NAT & for n holds f.n is PartFunc of D1,D2) proof thus f is Functional_Sequence of D1,D2 implies (dom f=NAT & for n holds f.n is PartFunc of D1,D2) by Lm1; assume that A1: dom f=NAT and A2: for n holds f.n is PartFunc of D1,D2; for x holds x in NAT implies f.x is PartFunc of D1,D2 by A2; hence thesis by A1,Lm1; end; Lm2: for F1,F2 st (for x st x in NAT holds F1.x = F2.x) holds F1 = F2 proof let F1,F2 such that A1: for x st x in NAT holds F1.x=F2.x; dom F1= NAT & dom F2=NAT by Def1; hence thesis by A1,FUNCT_1:9; end; theorem Th2: for F1,F2 st (for n holds F1.n = F2.n) holds F1 = F2 proof let F1,F2; assume for n holds F1.n=F2.n; then for x holds x in NAT implies F1.x=F2.x; hence thesis by Lm2; end; scheme ExFuncSeq{D1() -> non empty set, D2() -> non empty set, F(Nat)->PartFunc of D1(),D2()}: ex G being Functional_Sequence of D1(), D2() st for n holds G.n = F(n) proof defpred P[set,set] means ex n st (n=$1 & $2=F(n)); A1: now let x; assume x in NAT; then consider n such that A2: n=x; reconsider r2=F(n) as set; take y=r2; thus P[x,y] by A2; end; A3: for x,y,z st x in NAT & P[x,y] & P[x,z] holds y=z; consider f such that A4: dom f = NAT and A5: for x st x in NAT holds P[x,f.x] from FuncEx(A3,A1); now let x; assume x in NAT; then ex n st n=x & f.x=F(n) by A5; hence f.x is PartFunc of D1(),D2(); end; then reconsider f as Functional_Sequence of D1(),D2() by A4,Lm1; take f; let n; ex k st k=n & f.n=F(k) by A5; hence f.n=F(n); end; definition let D,H,r; func r(#)H ->Functional_Sequence of D,REAL means :Def2: for n holds it.n = r(#)(H.n); existence proof deffunc U(Nat) = r(#)(H.$1); thus ex f being Functional_Sequence of D,REAL st for n holds f.n = U(n) from ExFuncSeq; end; uniqueness proof let H1,H2 such that A1: for n holds H1.n=r(#)(H.n) and A2: for n holds H2.n=r(#)(H.n); now let n; H1.n=r(#)(H.n) & H2.n=r(#)(H.n) by A1,A2; hence H1.n=H2.n; end; hence H1=H2 by Th2; end; end; definition let D,H; func H" -> Functional_Sequence of D,REAL means :Def3: for n holds it.n=(H.n)^; existence proof deffunc U(Nat) = (H.$1)^; thus ex f being Functional_Sequence of D,REAL st for n holds f.n=U(n) from ExFuncSeq; end; uniqueness proof let H1,H2 such that A1: for n holds H1.n=(H.n)^ and A2: for n holds H2.n=(H.n)^; now let n; H1.n=(H.n)^ & H2.n=(H.n)^ by A1,A2; hence H1.n=H2.n; end; hence H1=H2 by Th2; end; func - H -> Functional_Sequence of D,REAL means :Def4: for n holds it.n = -H.n; existence proof take H1=(-1)(#)H; let n; thus H1.n=(-1)(#)H.n by Def2 .=-H.n by RFUNCT_1:38; end; uniqueness proof let H1,H2 such that A3: for n holds H1.n=-H.n and A4: for n holds H2.n=-H.n; now let n; H1.n=-H.n & H2.n=-H.n by A3,A4; hence H1.n=H2.n; end; hence H1=H2 by Th2; end; func abs(H)->Functional_Sequence of D,REAL means :Def5: for n holds it.n=abs(H.n); existence proof deffunc U(Nat) = abs(H.$1); thus ex f being Functional_Sequence of D,REAL st for n holds f.n=U(n) from ExFuncSeq; end; uniqueness proof let H1,H2 such that A5: for n holds H1.n=abs(H.n) and A6: for n holds H2.n=abs(H.n); now let n; H2.n=abs(H.n) by A6; hence H1.n=H2.n by A5; end; hence H1=H2 by Th2; end; end; definition let D,G,H; func G + H -> Functional_Sequence of D,REAL means :Def6: for n holds it.n = G.n + H.n; existence proof deffunc U(Nat) = G.$1 + H.$1; thus ex f being Functional_Sequence of D,REAL st for n holds f.n = U(n) from ExFuncSeq; end; uniqueness proof let H1,H2 such that A1: for n holds H1.n=G.n+H.n and A2: for n holds H2.n=G.n+H.n; now let n; H1.n=G.n+H.n & H2.n=G.n+H.n by A1,A2; hence H1.n=H2.n; end; hence H1=H2 by Th2; end; end; definition let D,G,H; func G - H -> Functional_Sequence of D,REAL equals :Def7: G + -H; correctness; end; definition let D,G,H; func G (#) H -> Functional_Sequence of D,REAL means :Def8: for n holds it.n =G.n (#) H.n; existence proof deffunc U(Nat) = G.$1 (#) H.$1; thus ex f being Functional_Sequence of D,REAL st for n holds f.n =U(n) from ExFuncSeq; end; uniqueness proof let H1,H2 such that A1: for n holds H1.n=G.n (#) H.n and A2: for n holds H2.n=G.n (#) H.n; now let n; H1.n=G.n(#)H.n & H2.n=G.n(#)H.n by A1,A2; hence H1.n=H2.n; end; hence H1=H2 by Th2; end; end; definition let D,H,G; func G / H ->Functional_Sequence of D,REAL equals :Def9: G (#) (H"); correctness; end; theorem H1 = G/H iff for n holds H1.n = G.n / H.n proof thus H1 = G/H implies for n holds H1.n = G.n / H.n proof assume A1: H1 = G/H; let n; thus H1.n = (G (#) (H")).n by A1,Def9 .= G.n (#) (H").n by Def8 .= G.n (#) ((H.n)^) by Def3 .= G.n / H.n by RFUNCT_1:47; end; assume A2: for n holds H1.n = G.n / H.n; now let n; thus H1.n = G.n / H.n by A2 .= G.n (#) ((H.n)^) by RFUNCT_1:47 .= G.n (#) (H").n by Def3 .= (G (#) (H")).n by Def8 .= (G/H).n by Def9; end; hence thesis by Th2; end; theorem Th4: H1 = G - H iff for n holds H1.n = G.n - H.n proof thus H1 = G - H implies for n holds H1.n = G.n - H.n proof assume A1: H1 = G - H; let n; thus H1.n = (G +-H).n by A1,Def7 .= G.n + (-H).n by Def6 .= G.n +- H.n by Def4 .= G.n - H.n by RFUNCT_1:40; end; assume A2: for n holds H1.n = G.n - H.n; now let n; thus H1.n = G.n - H.n by A2 .= G.n +- H.n by RFUNCT_1:40 .= G.n + (-H).n by Def4 .= (G +- H).n by Def6 .= (G - H).n by Def7; end; hence thesis by Th2; end; theorem G + H = H + G & (G + H) + J = G + (H + J) proof now let n; thus (G + H).n = H.n + G.n by Def6 .= (H + G).n by Def6; end; hence G + H = H + G by Th2; now let n; thus ((G + H) + J).n = (G + H).n + J.n by Def6 .= G.n + H.n + J.n by Def6 .= G.n + (H.n + J.n) by RFUNCT_1:19 .= G.n + (H + J).n by Def6 .= (G + (H + J)).n by Def6; end; hence thesis by Th2; end; theorem Th6: G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) proof now let n; thus (G (#) H).n = H.n (#) G.n by Def8 .= (H (#) G).n by Def8; end; hence G (#) H = H (#) G by Th2; now let n; thus ((G (#) H) (#) J).n = (G (#) H).n (#) J.n by Def8 .= G.n (#) H.n (#) J.n by Def8 .= G.n (#) (H.n (#) J.n) by RFUNCT_1:21 .= G.n (#) (H (#) J).n by Def8 .= (G (#) (H (#) J)).n by Def8; end; hence thesis by Th2; end; theorem (G + H) (#) J = G(#)J + H(#)J & J (#) (G + H) = J(#)G + J(#)H proof now let n; thus ((G + H) (#) J).n = (G + H).n (#) J.n by Def8 .= (G.n + H.n) (#) J.n by Def6 .= G.n (#) J.n + H.n (#) J.n by RFUNCT_1:22 .= (G(#)J).n + H.n (#) J.n by Def8 .= (G(#)J).n + (H(#)J).n by Def8 .= (G(#)J + H(#)J).n by Def6; end; hence (G + H) (#) J = G(#)J + H(#)J by Th2; hence J (#) (G + H) = G(#)J + H(#)J by Th6 .= J(#)G + H(#)J by Th6 .= J(#)G + J(#)H by Th6; end; theorem Th8: -H = (-1)(#)H proof now let n; thus (-H).n = -H.n by Def4 .=(-1) (#) H.n by RFUNCT_1:38 .=((-1)(#)H).n by Def2; end; hence thesis by Th2; end; theorem (G - H) (#) J = G(#)J - H(#)J & J(#)G - J(#)H = J (#) (G - H) proof now let n; thus ((G - H) (#) J).n = (G - H).n (#) J.n by Def8 .= (G.n - H.n) (#) J.n by Th4 .= G.n (#) J.n - H.n (#) J.n by RFUNCT_1:26 .= (G(#)J).n - H.n (#) J.n by Def8 .= (G(#)J).n - (H(#)J).n by Def8 .= (G(#)J - H(#)J).n by Th4; end; hence A1: (G - H) (#) J = G(#)J - H(#)J by Th2; thus J(#)G - J(#)H = J(#)G - H(#)J by Th6 .= (G - H) (#) J by A1,Th6 .= J (#) (G - H) by Th6; end; theorem r(#)(G + H) = r(#)G + r(#)H & r(#)(G - H) = r(#)G - r(#)H proof now let n; thus (r(#)(G + H)).n = r(#)(G + H).n by Def2 .= r(#)(G.n + H.n) by Def6 .= r(#)(G.n) + r(#)(H.n) by RFUNCT_1:28 .=(r(#)G).n + r(#)(H.n) by Def2 .=(r(#)G).n + (r(#)H).n by Def2 .=(r(#)G + r(#)H).n by Def6; end; hence r(#)(G + H) = r(#)G + r(#)H by Th2; now let n; thus (r(#)(G - H)).n = r(#)(G - H).n by Def2 .= r(#)(G.n - H.n) by Th4 .= r(#)G.n - r(#)H.n by RFUNCT_1:30 .= (r(#)G).n - r(#)H.n by Def2 .= (r(#)G).n - (r(#)H).n by Def2 .= (r(#)G - r(#)H).n by Th4; end; hence thesis by Th2; end; theorem Th11: (r*p)(#)H = r(#)(p(#)H) proof now let n; thus ((r*p)(#)H).n=(r*p)(#)H.n by Def2 .=r(#)(p(#)H.n) by RFUNCT_1:29 .=r(#)(p(#)H).n by Def2 .=(r(#)(p(#)H)).n by Def2; end; hence thesis by Th2; end; theorem Th12: 1 (#) H = H proof now let n; thus (1 (#) H).n = 1 (#) H.n by Def2 .= H.n by RFUNCT_1:33; end; hence thesis by Th2; end; theorem -(-H) = H proof thus -(-H) = (-1) (#) (-H) by Th8 .=(-1) (#) ((-1) (#) H) by Th8 .=((-1) * (-1)) (#) H by Th11 .=H by Th12; end; theorem G" (#) H" = (G(#)H)" proof now let n; thus (G" (#) H").n = (G".n) (#) (H".n) by Def8 .= ((G.n))^ (#) (H".n) by Def3 .= ((G.n)^) (#) ((H.n)^) by Def3 .= (G.n (#) H.n)^ by RFUNCT_1:43 .= ((G (#) H).n)^ by Def8 .= ((G (#) H)").n by Def3; end; hence thesis by Th2; end; theorem r<>0 implies (r(#)H)" = r" (#) H" proof assume A1: r<>0; now let n; thus (r(#)H)".n = ((r(#)H).n)^ by Def3 .= (r (#) H.n)^ by Def2 .= r" (#) ((H.n)^) by A1,RFUNCT_1:44 .= r" (#) (H".n) by Def3 .= (r" (#) H").n by Def2; end; hence thesis by Th2; end; theorem Th16: abs(H)"=abs(H") proof now let n; thus (abs(H")).n=abs(H".n) by Def5 .=abs((H.n)^) by Def3 .=(abs((H.n)))^ by RFUNCT_1:46 .=(abs(H).n)^ by Def5 .=(abs(H)").n by Def3; end; hence thesis by Th2; end; theorem Th17: abs(G(#)H) = abs(G) (#) abs(H) proof now let n; thus (abs(G(#)H)).n=abs(((G(#)H).n)) by Def5 .=abs((G.n)(#)(H.n)) by Def8 .=abs((G.n))(#)abs((H.n)) by RFUNCT_1:36 .=((abs(G)).n)(#)abs((H.n)) by Def5 .=((abs(G)).n)(#)(abs(H)).n by Def5 .=(abs(G)(#)abs(H)).n by Def8; end; hence thesis by Th2; end; theorem abs(G/H) = abs(G) / abs(H) proof thus abs(G/H)=abs(G (#) (H")) by Def9 .=abs(G)(#)abs((H")) by Th17 .=abs(G)(#)abs(H)" by Th16 .=abs(G)/abs(H) by Def9; end; theorem abs(r(#)H) = abs(r) (#) abs(H) proof now let n; thus abs(r(#)H).n=abs((r(#)H).n) by Def5 .=abs(r(#)(H.n)) by Def2 .=abs(r)(#)abs(H.n) by RFUNCT_1:37 .=abs(r)(#)(abs(H)).n by Def5 .=(abs(r)(#)abs(H)).n by Def2; end; hence thesis by Th2; end; reserve x for Element of D, X,Y for set, S1,S2 for Real_Sequence, f for PartFunc of D,REAL; definition let D1,D2,F,X; pred X common_on_dom F means :Def10: X <> {} & for n holds X c= dom (F.n); end; definition let D,H,x; func H#x ->Real_Sequence means :Def11: for n holds it.n = (H.n).x; existence proof deffunc U(Nat) = (H.$1).x; thus ex f being Real_Sequence st for n holds f.n = U(n) from ExRealSeq; end; uniqueness proof let S1,S2 such that A1: (for n holds S1.n = (H.n).x) & for n holds S2.n = (H.n).x; now let n; S1.n = (H.n).x & S2.n = (H.n).x by A1; hence S1.n = S2.n; end; hence thesis by FUNCT_2:113; end; end; definition let D,H,X; pred H is_point_conv_on X means :Def12: X common_on_dom H & ex f st X = dom f & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p; end; theorem Th20: H is_point_conv_on X iff X common_on_dom H & ex f st X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x proof thus H is_point_conv_on X implies X common_on_dom H & ex f st X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x proof assume A1: H is_point_conv_on X; hence X common_on_dom H by Def12; consider f such that A2: X = dom f & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p by A1,Def12; take f; thus X = dom f by A2; let x; assume A3: x in X; A4: now let p be real number; A5: p is Real by XREAL_0:def 1; assume p>0; then consider k such that A6: for n st n>=k holds abs((H.n).x - f.x) < p by A2,A3,A5; take k; let n; assume n>=k; then abs((H.n).x - f.x) < p by A6; hence abs((H#x).n - f.x) < p by Def11; end; hence (H#x) is convergent by SEQ_2:def 6; hence lim(H#x) = f.x by A4,SEQ_2:def 7; end; assume A7: X common_on_dom H; given f such that A8: X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x; ex f st X = dom f & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p proof take f; thus X = dom f by A8; let x; assume x in X; then A9: (H#x) is convergent & lim(H#x) = f.x by A8; let p; assume p>0; then consider k such that A10: for n st n>=k holds abs((H#x).n - f.x) < p by A9,SEQ_2:def 7; take k; let n; assume n >= k; then abs((H#x).n - f.x) < p by A10; hence abs((H.n).x - f.x) < p by Def11; end; hence thesis by A7,Def12; end; theorem Th21: H is_point_conv_on X iff X common_on_dom H & for x st x in X holds (H#x) is convergent proof thus H is_point_conv_on X implies X common_on_dom H & for x st x in X holds (H#x) is convergent proof assume A1: H is_point_conv_on X; hence X common_on_dom H by Def12; A2: ex f st X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x by A1,Th20; let x; assume x in X; hence (H#x) is convergent by A2; end; assume A3: X common_on_dom H & for x st x in X holds (H#x) is convergent; defpred X[set] means $1 in X; deffunc U(Element of D) = lim(H#$1); consider f such that A4: for x holds x in dom f iff X[x] and A5: for x st x in dom f holds f.x = U(x) from LambdaPFD'; now take f; thus A6: X = dom f proof thus X c= dom f proof let x be set such that A7: x in X; X c= dom (H.0) by A3,Def10; then X c= D by XBOOLE_1:1; then reconsider x' = x as Element of D by A7; x' in dom f by A4,A7; hence thesis; end; let x be set; assume x in dom f; hence thesis by A4; end; let x; assume A8: x in X; hence (H#x) is convergent by A3; thus f.x = lim(H#x) by A5,A6,A8; end; hence thesis by A3,Th20; end; definition let D,H,X; pred H is_unif_conv_on X means :Def13: X common_on_dom H & ex f st X = dom f & for p st p>0 ex k st for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p; end; definition let D,H,X; assume A1: H is_point_conv_on X; func lim(H,X) -> PartFunc of D,REAL means :Def14: dom it = X & for x st x in dom it holds it.x = lim(H#x); existence proof consider f such that A2: X = dom f & for x st x in X holds (H#x) is convergent & lim(H#x) = f.x by A1,Th20; take f; thus dom f = X by A2; let x; assume x in dom f; hence thesis by A2; end; uniqueness proof deffunc U(Element of D) = lim(H#$1); thus for f1,f2 be PartFunc of D,REAL st dom f1 = X & (for x st x in dom f1 holds f1.x = U(x))& dom f2 = X & for x st x in dom f2 holds f2.x = U(x) holds f1 = f2 from UnPartFuncD'; end; end; theorem Th22: H is_point_conv_on X implies (f = lim(H,X) iff dom f = X & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p) proof assume A1: H is_point_conv_on X; thus f = lim(H,X) implies dom f = X & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p proof assume A2: f = lim(H,X); hence A3: dom f = X by A1,Def14; let x; assume A4: x in X; then A5: f.x = lim(H#x) by A1,A2,A3,Def14; A6: H#x is convergent by A1,A4,Th21; let p; assume p>0; then consider k such that A7: for n st n>=k holds abs((H#x).n - f.x) < p by A5,A6,SEQ_2:def 7; take k; let n; assume n>=k; then abs((H#x).n - f.x) < p by A7; hence thesis by Def11; end; assume A8: dom f = X & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p; now let x such that A9: x in dom f; A10: now let p be real number; A11: p is Real by XREAL_0:def 1; assume p>0; then consider k such that A12: for n st n>=k holds abs((H.n).x - f.x) < p by A8,A9,A11; take k; let n; assume n >= k; then abs((H.n).x - f.x) < p by A12; hence abs((H#x).n - f.x) < p by Def11; end; then H#x is convergent by SEQ_2:def 6; hence f.x = lim(H#x) by A10,SEQ_2:def 7; end; hence thesis by A1,A8,Def14; end; theorem Th23: H is_unif_conv_on X implies H is_point_conv_on X proof assume A1: H is_unif_conv_on X; then A2: X common_on_dom H by Def13; now consider f such that A3: X = dom f & for p st p>0 ex k st for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A1,Def13; take f; thus X = dom f by A3; let x; assume A4: x in X; let p; assume p>0; then consider k such that A5: for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A3; take k; let n; assume n>=k; hence abs((H.n).x - f.x) < p by A4,A5; end; hence thesis by A2,Def12; end; theorem Th24: Y c= X & Y<>{} & X common_on_dom H implies Y common_on_dom H proof assume A1: Y c= X & Y<>{} & X common_on_dom H; now let n; X c= dom (H.n) by A1,Def10; hence Y c= dom (H.n) by A1,XBOOLE_1:1; end; hence thesis by A1,Def10; end; theorem Y c= X & Y<>{} & H is_point_conv_on X implies H is_point_conv_on Y & lim(H,X)|Y = lim(H,Y) proof assume A1: Y c= X & Y<>{} & H is_point_conv_on X; then X common_on_dom H by Def12; then A2: Y common_on_dom H by A1,Th24; consider f such that A3: X = dom f & for x st x in X holds for p st p>0 ex k st for n st n>=k holds abs((H.n).x - f.x) < p by A1,Def12; now take g = f|Y; thus A4: Y = dom g by A1,A3,RELAT_1:91; let x; assume A5: x in Y; let p; assume p>0; then consider k such that A6: for n st n>=k holds abs((H.n).x - f.x) < p by A1,A3,A5; take k; let n; assume n>=k; then abs((H.n).x - f.x) < p by A6; hence abs((H.n).x - g.x) < p by A4,A5,FUNCT_1:68; end; hence A7: H is_point_conv_on Y by A2,Def12; dom lim(H,X) = X by A1,Def14; then dom lim(H,X) /\ Y = Y by A1,XBOOLE_1:28; then dom (lim(H,X)|Y) = Y by RELAT_1:90; then A8: dom (lim(H,X)|Y) = dom lim(H,Y) by A7,Def14; now let x; assume A9: x in dom (lim(H,X)|Y); then x in (dom lim(H,X)) /\ Y by RELAT_1:90; then A10: x in dom lim(H,X) & x in Y by XBOOLE_0:def 3; then A11: x in dom lim(H,Y) by A7,Def14; thus (lim(H,X)|Y).x = (lim(H,X)).x by A9,FUNCT_1:68 .= lim (H#x) by A1,A10,Def14 .= (lim(H,Y)).x by A7,A11,Def14; end; hence thesis by A8,PARTFUN1:34; end; theorem Y c= X & Y<>{} & H is_unif_conv_on X implies H is_unif_conv_on Y proof assume A1: Y c= X & Y<>{} & H is_unif_conv_on X; then X common_on_dom H by Def13; then A2: Y common_on_dom H by A1,Th24; consider f such that A3: dom f = X & for p st p>0 ex k st for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A1,Def13; now take g = f|Y; thus A4: dom g = dom f /\ Y by RELAT_1:90 .= Y by A1,A3,XBOOLE_1:28; let p; assume p>0; then consider k such that A5: for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A3; take k; let n,x; assume A6: n>=k & x in Y; then abs((H.n).x - f.x) < p by A1,A5; hence abs((H.n).x - g.x) < p by A4,A6,FUNCT_1:68; end; hence thesis by A2,Def13; end; theorem Th27: X common_on_dom H implies for x st x in X holds {x} common_on_dom H proof assume A1: X common_on_dom H; let x; assume A2: x in X; thus {x} <> {} by TARSKI:def 1; now let n; X c= dom(H.n) by A1,Def10; hence {x} c= dom(H.n) by A2,ZFMISC_1:37; end; hence thesis; end; theorem H is_point_conv_on X implies for x st x in X holds {x} common_on_dom H proof assume H is_point_conv_on X; then X common_on_dom H by Def12; hence thesis by Th27; end; theorem Th29: {x} common_on_dom H1 & {x} common_on_dom H2 implies H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x) = (H1(#)H2)#x proof assume A1: {x} common_on_dom H1 & {x} common_on_dom H2; now let n; A2: x in {x} by TARSKI:def 1; {x} c= dom(H1.n) & {x} c= dom (H2.n) by A1,Def10; then x in (dom(H1.n) /\ dom(H2.n)) by A2,XBOOLE_0:def 3; then A3: x in dom(H1.n + H2.n) by SEQ_1:def 3; thus (H1#x + H2#x).n = (H1#x).n + (H2#x).n by SEQ_1:11 .= (H1.n).x + (H2#x).n by Def11 .= (H1.n).x + (H2.n).x by Def11 .= ((H1.n) + (H2.n)).x by A3,SEQ_1:def 3 .= ((H1+H2).n).x by Def6 .= ((H1+H2)#x).n by Def11; end; hence H1#x + H2#x = (H1+H2)#x by FUNCT_2:113; now let n; A4: x in {x} by TARSKI:def 1; {x} c= dom(H1.n) & {x} c= dom (H2.n) by A1,Def10; then x in (dom(H1.n) /\ dom(H2.n)) by A4,XBOOLE_0:def 3; then A5: x in dom(H1.n - H2.n) by SEQ_1:def 4; thus (H1#x - H2#x).n = (H1#x).n - (H2#x).n by RFUNCT_2:6 .= (H1.n).x - (H2#x).n by Def11 .= (H1.n).x - (H2.n).x by Def11 .= ((H1.n) - (H2.n)).x by A5,SEQ_1:def 4 .= ((H1-H2).n).x by Th4 .= ((H1-H2)#x).n by Def11; end; hence H1#x - H2#x = (H1-H2)#x by FUNCT_2:113; now let n; A6: x in {x} by TARSKI:def 1; {x} c= dom(H1.n) & {x} c= dom (H2.n) by A1,Def10; then x in (dom(H1.n) /\ dom(H2.n)) by A6,XBOOLE_0:def 3; then A7: x in dom(H1.n (#) H2.n) by SEQ_1:def 5; thus ((H1#x) (#) (H2#x)).n = (H1#x).n * (H2#x).n by SEQ_1:12 .= (H1.n).x * (H2#x).n by Def11 .= (H1.n).x * (H2.n).x by Def11 .= ((H1.n) (#) (H2.n)).x by A7,SEQ_1:def 5 .= ((H1(#)H2).n).x by Def8 .= ((H1(#)H2)#x).n by Def11; end; hence thesis by FUNCT_2:113; end; theorem Th30: {x} common_on_dom H implies (abs(H))#x = abs(H#x) & (-H)#x = -(H#x) proof assume A1: {x} common_on_dom H; now let n; A2: x in {x} by TARSKI:def 1; {x} c= dom(H.n) by A1,Def10; then x in dom (H.n) by A2; then A3: x in dom (abs(H.n)) by SEQ_1:def 10; thus ((abs(H))#x).n = (abs(H).n).x by Def11 .= abs((H.n)).x by Def5 .= abs((H.n).x) by A3,SEQ_1:def 10 .= abs((H#x).n) by Def11 .= abs((H#x)).n by SEQ_1:16; end; hence (abs(H))#x = abs((H#x)) by FUNCT_2:113; now let n; A4: x in {x} by TARSKI:def 1; {x} c= dom(H.n) by A1,Def10; then x in dom (H.n) by A4; then A5: x in dom (-(H.n)) by SEQ_1:def 7; thus ((-H)#x).n = ((-H).n).x by Def11 .= (-H.n).x by Def4 .= -((H.n).x) by A5,SEQ_1:def 7 .= -((H#x).n) by Def11 .= (-(H#x)).n by SEQ_1:14; end; hence thesis by FUNCT_2:113; end; theorem Th31: {x} common_on_dom H implies (r(#)H)#x = r(#)(H#x) proof assume A1: {x} common_on_dom H; now let n; A2: x in {x} by TARSKI:def 1; {x} c= dom(H.n) by A1,Def10; then x in dom (H.n) by A2; then A3: x in dom (r(#)(H.n)) by SEQ_1:def 6; thus ((r(#)H)#x).n = ((r(#)H).n).x by Def11 .= (r(#)(H.n)).x by Def2 .= r*((H.n).x) by A3,SEQ_1:def 6 .= r*((H#x).n) by Def11 .= (r(#)(H#x)).n by SEQ_1:13; end; hence thesis by FUNCT_2:113; end; theorem Th32: X common_on_dom H1 & X common_on_dom H2 implies for x st x in X holds H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x) = (H1(#)H2)#x proof assume A1: X common_on_dom H1 & X common_on_dom H2; let x; assume A2: x in X; then A3: {x} common_on_dom H1 by A1,Th27; {x} common_on_dom H2 by A1,A2,Th27; hence thesis by A3,Th29; end; theorem Th33: X common_on_dom H implies for x st x in X holds abs(H)#x = abs(H#x) & (-H)#x = -(H#x) proof assume A1: X common_on_dom H; let x; assume x in X; then {x} common_on_dom H by A1,Th27; hence thesis by Th30; end; theorem Th34: X common_on_dom H implies for x st x in X holds (r(#)H)#x = r(#)(H#x) proof assume A1: X common_on_dom H; let x; assume x in X; then {x} common_on_dom H by A1,Th27; hence thesis by Th31; end; theorem Th35: H1 is_point_conv_on X & H2 is_point_conv_on X implies for x st x in X holds H1#x + H2#x = (H1+H2)#x & H1#x - H2#x = (H1-H2)#x & (H1#x) (#) (H2#x) = (H1(#)H2)#x proof assume A1: H1 is_point_conv_on X & H2 is_point_conv_on X; then A2: X common_on_dom H1 by Def12; X common_on_dom H2 by A1,Def12; hence thesis by A2,Th32; end; theorem Th36: H is_point_conv_on X implies for x st x in X holds abs(H)#x = abs(H#x) & (-H)#x = -(H#x) proof assume H is_point_conv_on X; then X common_on_dom H by Def12; hence thesis by Th33; end; theorem H is_point_conv_on X implies for x st x in X holds (r(#)H)#x = r(#)(H#x) proof assume H is_point_conv_on X; then X common_on_dom H by Def12; hence thesis by Th34; end; theorem Th38: X common_on_dom H1 & X common_on_dom H2 implies X common_on_dom H1+H2 & X common_on_dom H1-H2 & X common_on_dom H1(#)H2 proof assume A1: X common_on_dom H1 & X common_on_dom H2; then A2: X <> {} by Def10; now let n; A3: X c= dom (H1.n) by A1,Def10; X c= dom (H2.n) by A1,Def10; then X c= dom (H1.n) /\ dom (H2.n) by A3,XBOOLE_1:19; then X c= dom (H1.n + H2.n) by SEQ_1:def 3; hence X c= dom ((H1+H2).n) by Def6; end; hence X common_on_dom H1+H2 by A2,Def10; now let n; A4: X c= dom (H1.n) by A1,Def10; X c= dom (H2.n) by A1,Def10; then X c= dom (H1.n) /\ dom (H2.n) by A4,XBOOLE_1:19; then X c= dom (H1.n - H2.n) by SEQ_1:def 4; hence X c= dom ((H1-H2).n) by Th4; end; hence X common_on_dom H1-H2 by A2,Def10; now let n; A5: X c= dom (H1.n) by A1,Def10; X c= dom (H2.n) by A1,Def10; then X c= dom (H1.n) /\ dom (H2.n) by A5,XBOOLE_1:19; then X c= dom (H1.n (#) H2.n) by SEQ_1:def 5; hence X c= dom ((H1(#)H2).n) by Def8; end; hence thesis by A2,Def10; end; theorem Th39: X common_on_dom H implies X common_on_dom abs(H) & X common_on_dom (-H) proof assume A1: X common_on_dom H; then A2: X <> {} by Def10; now let n; dom (H.n) = dom (abs(H.n)) by SEQ_1:def 10 .= dom (abs(H).n) by Def5; hence X c= dom (abs(H).n) by A1,Def10; end; hence X common_on_dom abs(H) by A2,Def10; now let n; dom (H.n) = dom (-(H.n)) by SEQ_1:def 7 .= dom ((-H).n) by Def4; hence X c= dom ((-H).n) by A1,Def10; end; hence thesis by A2,Def10; end; theorem Th40: X common_on_dom H implies X common_on_dom r(#)H proof assume A1: X common_on_dom H; then A2: X <> {} by Def10; now let n; dom (H.n) = dom(r(#)(H.n)) by SEQ_1:def 6 .= dom ((r(#)H).n) by Def2; hence X c= dom ((r(#)H).n) by A1,Def10; end; hence thesis by A2,Def10; end; theorem H1 is_point_conv_on X & H2 is_point_conv_on X implies H1+H2 is_point_conv_on X & lim(H1+H2,X) = lim(H1,X) + lim(H2,X) & H1-H2 is_point_conv_on X & lim(H1-H2,X) = lim(H1,X) - lim(H2,X) & H1(#)H2 is_point_conv_on X & lim(H1(#)H2,X) = lim(H1,X) (#) lim(H2,X) proof assume A1: H1 is_point_conv_on X & H2 is_point_conv_on X; then A2: X common_on_dom H1 & for x st x in X holds H1#x is convergent by Th21; X common_on_dom H2 & for x st x in X holds H2#x is convergent by A1,Th21; then A3: X common_on_dom H1+H2 & X common_on_dom H1-H2 & X common_on_dom H1 (#)H2 by A2,Th38; now let x; assume A4: x in X; then A5: H1#x is convergent by A1,Th21; H2#x is convergent by A1,A4,Th21; then (H1#x)+(H2#x) is convergent by A5,SEQ_2:19; hence (H1+H2)#x is convergent by A1,A4,Th35; end; hence A6: H1+H2 is_point_conv_on X by A3,Th21; A7: dom (lim(H1,X)+lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by SEQ_1:def 3 .= X /\ (dom lim(H2,X)) by A1,Def14 .= X /\ X by A1,Def14 .= X; now let x; assume A8: x in dom (lim(H1,X)+lim(H2,X)); then x in (dom lim(H1,X))/\(dom lim(H2,X)) by SEQ_1:def 3; then A9: x in (dom lim(H1,X)) & x in (dom lim(H2,X)) by XBOOLE_0:def 3; then A10: x in X by A1,Def14; then A11: H1#x is convergent by A1,Th21; A12: H2#x is convergent by A1,A10,Th21; thus (lim(H1,X) + lim(H2,X)).x = (lim(H1,X)).x + (lim(H2,X)).x by A8,SEQ_1:def 3 .= lim(H1#x) + (lim(H2,X)).x by A1,A9,Def14 .= lim(H1#x) + lim(H2#x) by A1,A9,Def14 .= lim((H1#x) + (H2#x)) by A11,A12,SEQ_2:20 .= lim((H1+H2)#x) by A1,A10,Th35; end; hence lim(H1+H2,X) = lim(H1,X) + lim(H2,X) by A6,A7,Def14; now let x; assume A13: x in X; then A14: H1#x is convergent by A1,Th21; H2#x is convergent by A1,A13,Th21; then (H1#x)-(H2#x) is convergent by A14,SEQ_2:25; hence (H1-H2)#x is convergent by A1,A13,Th35; end; hence A15: H1-H2 is_point_conv_on X by A3,Th21; A16: dom (lim(H1,X)-lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by SEQ_1:def 4 .= X /\ (dom lim(H2,X)) by A1,Def14 .= X /\ X by A1,Def14 .= X; now let x; assume A17: x in dom (lim(H1,X)-lim(H2,X)); then x in (dom lim(H1,X))/\(dom lim(H2,X)) by SEQ_1:def 4; then A18: x in (dom lim(H1,X)) & x in (dom lim(H2,X)) by XBOOLE_0:def 3; then A19: x in X by A1,Def14; then A20: H1#x is convergent by A1,Th21; A21: H2#x is convergent by A1,A19,Th21; thus (lim(H1,X) - lim(H2,X)).x = (lim(H1,X)).x - (lim(H2,X)).x by A17,SEQ_1:def 4 .= lim(H1#x) - (lim(H2,X)).x by A1,A18,Def14 .= lim(H1#x) - lim(H2#x) by A1,A18,Def14 .= lim((H1#x) - (H2#x)) by A20,A21,SEQ_2:26 .= lim((H1-H2)#x) by A1,A19,Th35; end; hence lim(H1-H2,X) = lim(H1,X) - lim(H2,X) by A15,A16,Def14; now let x; assume A22: x in X; then A23: H1#x is convergent by A1,Th21; H2#x is convergent by A1,A22,Th21; then (H1#x)(#)(H2#x) is convergent by A23,SEQ_2:28; hence (H1(#)H2)#x is convergent by A1,A22,Th35; end; hence A24: H1(#)H2 is_point_conv_on X by A3,Th21; A25: dom (lim(H1,X)(#)lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by SEQ_1:def 5 .= X /\ (dom lim(H2,X)) by A1,Def14 .= X /\ X by A1,Def14 .= X; now let x; assume A26: x in dom (lim(H1,X)(#)lim(H2,X)); then x in (dom lim(H1,X))/\(dom lim(H2,X)) by SEQ_1:def 5; then A27: x in (dom lim(H1,X)) & x in (dom lim(H2,X)) by XBOOLE_0:def 3; then A28: x in X by A1,Def14; then A29: H1#x is convergent by A1,Th21; A30: H2#x is convergent by A1,A28,Th21; thus (lim(H1,X) (#) lim(H2,X)).x = (lim(H1,X)).x * (lim(H2,X)).x by A26,SEQ_1:def 5 .= lim(H1#x) * (lim(H2,X)).x by A1,A27,Def14 .= lim(H1#x) * lim(H2#x) by A1,A27,Def14 .= lim((H1#x) (#) (H2#x)) by A29,A30,SEQ_2:29 .= lim((H1(#)H2)#x) by A1,A28,Th35; end; hence thesis by A24,A25,Def14; end; theorem H is_point_conv_on X implies abs(H) is_point_conv_on X & lim (abs(H),X) = abs( lim (H,X) ) & -H is_point_conv_on X & lim (-H,X) = - lim(H,X) proof assume A1: H is_point_conv_on X; then A2: X common_on_dom H & for x st x in X holds H#x is convergent by Th21; then A3: X common_on_dom abs(H) by Th39; now let x; assume A4: x in X; then H#x is convergent by A1,Th21; then abs(H#x) is convergent by SEQ_4:26; hence abs(H)#x is convergent by A2,A4,Th33; end; hence A5: abs(H) is_point_conv_on X by A3,Th21; A6: dom abs(lim(H,X)) = dom lim(H,X) by SEQ_1:def 10 .= X by A1,Def14; now let x; assume A7: x in dom abs(lim(H,X)); then A8: x in dom lim(H,X) by SEQ_1:def 10; then A9: x in X by A1,Def14; then A10: H#x is convergent by A1,Th21; thus abs(lim(H,X)).x = abs(lim(H,X).x) by A7,SEQ_1:def 10 .= abs(lim(H#x)) by A1,A8,Def14 .= lim abs((H#x)) by A10,SEQ_4:27 .= lim(abs(H)#x) by A1,A9,Th36; end; hence lim (abs(H),X) = abs( lim (H,X) ) by A5,A6,Def14; A11: X common_on_dom -H by A2,Th39; now let x; assume A12: x in X; then H#x is convergent by A1,Th21; then -(H#x) is convergent by SEQ_2:23; hence (-H)#x is convergent by A2,A12,Th33; end; hence A13: -H is_point_conv_on X by A11,Th21; A14: dom (-lim(H,X)) = dom lim(H,X) by SEQ_1:def 7 .= X by A1,Def14; now let x; assume A15: x in dom (-lim(H,X)); then A16: x in dom lim(H,X) by SEQ_1:def 7; then A17: x in X by A1,Def14; then A18: H#x is convergent by A1,Th21; thus (-lim(H,X)).x = -(lim(H,X).x) by A15,SEQ_1:def 7 .= -(lim(H#x)) by A1,A16,Def14 .= lim(-(H#x)) by A18,SEQ_2:24 .= lim((-H)#x) by A1,A17,Th36; end; hence thesis by A13,A14,Def14; end; theorem H is_point_conv_on X implies r(#)H is_point_conv_on X & lim (r(#)H,X) = r(#)(lim(H,X)) proof assume A1: H is_point_conv_on X; then A2: X common_on_dom H & for x st x in X holds H#x is convergent by Th21; then A3: X common_on_dom r(#)H by Th40; now let x; assume A4: x in X; then H#x is convergent by A1,Th21; then r(#)(H#x) is convergent by SEQ_2:21; hence (r(#)H)#x is convergent by A2,A4,Th34; end; hence A5: r(#)H is_point_conv_on X by A3,Th21; A6: dom(r(#)(lim(H,X))) = dom lim(H,X) by SEQ_1:def 6 .= X by A1,Def14; now let x; assume A7: x in dom(r(#)(lim(H,X))); then A8: x in dom lim(H,X) by SEQ_1:def 6; then A9: x in X by A1,Def14; then A10: H#x is convergent by A1,Th21; thus (r(#)lim(H,X)).x = r*(lim(H,X).x) by A7,SEQ_1:def 6 .= r*(lim(H#x)) by A1,A8,Def14 .= lim(r(#)(H#x)) by A10,SEQ_2:22 .= lim((r(#)H)#x) by A2,A9,Th34; end; hence thesis by A5,A6,Def14; end; theorem Th44: H is_unif_conv_on X iff X common_on_dom H & H is_point_conv_on X & for r st 0<r ex k st for n,x st n>=k & x in X holds abs((H.n).x-(lim(H,X)).x)<r proof thus H is_unif_conv_on X implies X common_on_dom H & H is_point_conv_on X & for r st 0<r ex k st for n,x st n>=k & x in X holds abs((H.n).x-(lim(H,X)).x)<r proof assume A1: H is_unif_conv_on X; then consider f such that A2: X = dom f & for p st p>0 ex k st for n,x st n>= k & x in X holds abs((H.n).x-f.x)<p by Def13; A3: now let x such that A4: x in X; let p; assume p>0; then consider k such that A5: for n,x st n>=k & x in X holds abs((H.n).x-f.x)<p by A2; take k; let n; assume n>=k; hence abs((H.n).x-f.x)<p by A4,A5; end; thus X common_on_dom H by A1,Def13; thus H is_point_conv_on X by A1,Th23; then A6: f = (lim(H,X)) by A2,A3,Th22; let r; assume r > 0; then consider k such that A7: for n,x st n>=k & x in X holds abs((H.n).x-f.x)<r by A2; take k; let n,x; assume n>=k & x in X; hence thesis by A6,A7; end; assume A8: X common_on_dom H & H is_point_conv_on X & for r st 0<r ex k st for n,x st n>=k & x in X holds abs((H.n).x-(lim(H,X)).x)<r; then dom lim(H,X) = X by Def14; hence thesis by A8,Def13; end; reserve H for Functional_Sequence of REAL,REAL; theorem H is_unif_conv_on X & (for n holds H.n is_continuous_on X) implies lim(H,X) is_continuous_on X proof set l = lim(H,X); assume A1: H is_unif_conv_on X & for n holds H.n is_continuous_on X; then A2: H is_point_conv_on X by Th23; then A3: dom l = X by Def14; A4: X common_on_dom H by A1,Def13; for x0 be real number st x0 in X holds l|X is_continuous_in x0 proof let x0 be real number; assume A5: x0 in X; then A6: x0 in dom(l|X) by A3,RELAT_1:97; reconsider x0 as Real by XREAL_0:def 1; for r be real number st 0<r ex s be real number st 0<s & for x1 be real number st x1 in dom (l|X) & abs(x1-x0)<s holds abs((l|X).x1-(l|X).x0)<r proof let r be real number; assume 0<r; then A7: 0 < r/3 by SEQ_4:4; reconsider r as Real by XREAL_0:def 1; consider k such that A8: for n,x1 st n>=k & x1 in X holds abs((H.n).x1-l.x1)<r/3 by A1,A7,Th44; consider k1 be Nat such that A9: for n st n>=k1 holds abs((H.n).x0 - l.x0) < r/3 by A2,A5,A7,Th22; set m = max(k,k1); set h = H.m; A10: m >= k & m >= k1 by SQUARE_1:46; h is_continuous_on X by A1; then h|X is_continuous_in x0 by A5,FCONT_1:def 2; then consider s be real number such that A11: 0<s & for x1 be real number st x1 in dom (h|X) & abs(x1-x0)<s holds abs((h|X).x1-(h|X).x0)<r/3 by A7,FCONT_1:3; reconsider s as Real by XREAL_0:def 1; take s; thus 0<s by A11; A12: dom (l|X) = dom l /\ X by RELAT_1:90 .= X by A3; let x1 be real number; assume A13: x1 in dom (l|X) & abs(x1-x0)<s; then abs(h.x1-l.x1)<r/3 by A8,A10,A12; then abs(-(l.x1-h.x1))<r/3 by XCMPLX_1:143; then A14: abs(l.x1-h.x1)<r/3 by ABSVALUE:17; A15: X c= dom h & X c= X by A4,Def10; A16: dom(h|X) = dom h /\ X by RELAT_1:90 .= X by A15,XBOOLE_1:28; then abs((h|X).x1-(h|X).x0)<r/3 by A11,A12,A13; then abs(h.x1-(h|X).x0)<r/3 by A12,A13,A16,FUNCT_1:68; then A17: abs(h.x1-h.x0)<r/3 by A5,FUNCT_1:72; A18:abs(h.x0 - l.x0) < r/3 by A9,A10; abs(l.x1 - l.x0) = abs((l.x1-h.x1)+(h.x1-l.x0)) by XCMPLX_1:39 .= abs((l.x1-h.x1)+((h.x1-h.x0)+(h.x0-l.x0))) by XCMPLX_1:39; then A19: abs(l.x1 - l.x0) <= abs(l.x1-h.x1)+ abs((h.x1-h.x0)+(h.x0-l.x0) ) by ABSVALUE:13; A20: abs((h.x1-h.x0)+(h.x0-l.x0))<=abs(h.x1-h.x0)+abs(h.x0-l.x0) by ABSVALUE:13; abs(h.x1-h.x0)+abs(h.x0-l.x0) < r/3 + r/3 by A17,A18,REAL_1:67; then abs((h.x1-h.x0)+(h.x0-l.x0))<r/3+r/3 by A20,AXIOMS:22; then abs(l.x1-h.x1)+ abs((h.x1-h.x0)+(h.x0-l.x0)) < r/3 +(r/3+r/3) by A14,REAL_1:67; then abs(l.x1 - l.x0) < r/3 +r/3+r/3 by A19,AXIOMS:22; then abs(l.x1 - l.x0) < r by XCMPLX_1:69; then abs((l|X).x1 - l.x0) < r by A13,FUNCT_1:68; hence thesis by A3,RELAT_1:97; end; hence thesis by A6,FCONT_1:3; end; hence thesis by A3,FCONT_1:def 2; end;

Back to top