:: Functional Sequence from a Domain to a Domain
::  by Beata Perkowska
::
:: Received May 22, 1992
:: Copyright (c) 1992-2012 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 XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, FUNCT_1, NAT_1, PARTFUN1,
      ORDINAL1, RELAT_1, TARSKI, XREAL_0, VALUED_1, ORDINAL4, ARYTM_1,
      COMPLEX1, ARYTM_3, CARD_1, SEQ_1, PBOOLE, XXREAL_0, SEQ_2, ORDINAL2,
      FCONT_1, SEQFUNC;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
      COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, RFUNCT_1,
      VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, FCONT_1;
 constructors PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, SEQ_2, RFUNCT_1, FCONT_1,
      LIMFUNC1, VALUED_1, SEQ_1, RELSET_1, COMSEQ_2;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
      VALUED_0, VALUED_1, FUNCT_2, PARTFUN1, COMSEQ_2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, VALUED_1;
 theorems FUNCT_1, PARTFUN1, TARSKI, RFUNCT_1, SEQ_1, SEQ_2, SEQ_4, ZFMISC_1,
      RFUNCT_2, FCONT_1, FUNCT_2, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
      XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, VALUED_1, RELSET_1;
 schemes CLASSES1, SEQ_1;

begin

reserve D for non empty set,
  D1,D2,x,y for set,
  n,k for Element of NAT,
  p,x1 ,r for Real,
  f for Function;

definition
  let D1,D2;
  mode Functional_Sequence of D1,D2 is sequence of PFuncs(D1,D2);
end;

reserve F for Functional_Sequence of D1,D2;

definition
  let D1,D2,F;
  let n be Nat;
  redefine func F.n -> PartFunc of D1,D2;
  coherence
  proof
    n in NAT by ORDINAL1:def 12;
    then n in dom F by FUNCT_2:def 1;
    then F.n in rng F by FUNCT_1:def 3;
    hence thesis by PARTFUN1:46;
  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 FUNCT_2:def 1;
    let x;
    assume x in NAT;
    then x in dom f by A1,FUNCT_2:def 1;
    then
A2: f.x in rng f by FUNCT_1:def 3;
    rng f c=PFuncs(D1,D2) by A1,RELAT_1:def 19;
    hence thesis by A2,PARTFUN1:46;
  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 3;
    f.x is PartFunc of D1,D2 by A3,A4,A5;
    hence y in PFuncs(D1,D2) by A6,PARTFUN1:45;
  end;
  then rng f c=PFuncs(D1,D2) by TARSKI:def 3;
  hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
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;

scheme
  ExFuncSeq{D1() -> set, D2() -> set, F(set)->PartFunc of D1(),D2()}: ex G
  being Functional_Sequence of D1(), D2() st for n being Nat holds G.n = F(n)
proof
  defpred P[set,set] means $2=F($1);
A1: for x st x in NAT ex y st P[x,y];
  consider f such that
A2: dom f = NAT and
A3: for x st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A1);
  now
    let x;
    assume x in NAT;
    then f.x=F(x) by A3;
    hence f.x is PartFunc of D1(),D2();
  end;
  then reconsider f as Functional_Sequence of D1(),D2() by A2,Lm1;
  take f;
  let n be Nat;
  n in NAT by ORDINAL1:def 12;
  hence thesis by A3;
end;

definition
  let D,H;

  let r be real number;
  func r(#)H ->Functional_Sequence of D,REAL means
  :Def1:
  for n being Nat 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 being Nat holds f.n
    = U(n) from ExFuncSeq;
  end;
  uniqueness
  proof
    let H1,H2 such that
A1: for n being Nat holds H1.n=r(#)(H.n) and
A2: for n being Nat holds H2.n=r(#)(H.n);
    now
      let n;
      H1.n=r(#)(H.n) by A1;
      hence H1.n=H2.n by A2;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
end;

definition
  let D,H;
  func H" -> Functional_Sequence of D,REAL means
  :Def2:
  for n being Nat holds it.n=(H.n)^;
  existence
  proof
    deffunc U(Nat) = (H.$1)^;
    thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f.n
    =U(n) from ExFuncSeq;
  end;
  uniqueness
  proof
    let H1,H2 such that
A1: for n being Nat holds H1.n=(H.n)^ and
A2: for n being Nat holds H2.n=(H.n)^;
    now
      let n;
      H1.n=(H.n)^ by A1;
      hence H1.n=H2.n by A2;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
  func - H -> Functional_Sequence of D,REAL means
  :Def3:
  for n being Nat holds it.n = -H.n;
  existence
  proof
    take (-1)(#)H;
    let n be Nat;
    thus thesis by Def1;
  end;
  uniqueness
  proof
    let H1,H2 such that
A3: for n being Nat holds H1.n=-H.n and
A4: for n being Nat holds H2.n=-H.n;
    now
      let n;
      H1.n=-H.n by A3;
      hence H1.n=H2.n by A4;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
 involutiveness
  proof let G,H be Functional_Sequence of D,REAL such that
A5:  for n being Nat holds G.n=-(H.n);
   let n be Nat;
   thus H.n = --(H.n)
      .= -(G.n) by A5;
  end;
  func abs(H)->Functional_Sequence of D,REAL means
  :Def4:
  for n being Nat 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 being Nat holds f.n
    =U(n) from ExFuncSeq;
  end;
  uniqueness
  proof
    let H1,H2 such that
A6: for n being Nat holds H1.n=abs(H.n) and
A7: for n being Nat holds H2.n=abs(H.n);
    now
      let n;
      H2.n=abs(H.n) by A7;
      hence H1.n=H2.n by A6;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
 projectivity
  proof let G,H be Functional_Sequence of D,REAL such that
A8:  for n being Nat holds G.n= abs(H.n);
   let n be Nat;
   thus G.n = abs abs(H.n) by A8
      .= abs(G.n) by A8;
  end;
end;

definition
  let D,G,H;
  func G + H -> Functional_Sequence of D,REAL means
  :Def5:
  for n being Nat 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 being Nat holds f.n
    = U(n) from ExFuncSeq;
  end;
  uniqueness
  proof
    let H1,H2 such that
A1: for n being Nat holds H1.n=G.n+H.n and
A2: for n being Nat holds H2.n=G.n+H.n;
    now
      let n;
      H1.n=G.n+H.n by A1;
      hence H1.n=H2.n by A2;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
end;

definition
  let D,G,H;
  func G - H -> Functional_Sequence of D,REAL equals
  G + -H;
  correctness;
end;

definition
  let D,G,H;
  func G (#) H -> Functional_Sequence of D,REAL means
  :Def7:
  for n being Nat 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 being Nat holds f.n
    =U(n) from ExFuncSeq;
  end;
  uniqueness
  proof
    let H1,H2 such that
A1: for n being Nat holds H1.n=G.n (#) H.n and
A2: for n being Nat holds H2.n=G.n (#) H.n;
    now
      let n;
      H1.n=G.n(#)H.n by A1;
      hence H1.n=H2.n by A2;
    end;
    hence H1=H2 by FUNCT_2:63;
  end;
end;

definition
  let D,H,G;
  func G / H ->Functional_Sequence of D,REAL equals
  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.n (#) (H").n by A1,Def7
      .= G.n (#) ((H.n)^) by Def2
      .= G.n / H.n by RFUNCT_1:31;
  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:31
      .= G.n (#) (H").n by Def2
      .= (G/H).n by Def7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th3:
  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.n + (-H).n by A1,Def5
      .= G.n - H.n by Def3;
  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 Def3
      .= (G - H).n by Def5;
  end;
  hence thesis by FUNCT_2:63;
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 Def5
      .= (H + G).n by Def5;
  end;
  hence G + H = H + G by FUNCT_2:63;
  now
    let n;
    thus ((G + H) + J).n = (G + H).n + J.n by Def5
      .= G.n + H.n + J.n by Def5
      .= G.n + (H.n + J.n) by RFUNCT_1:8
      .= G.n + (H + J).n by Def5
      .= (G + (H + J)).n by Def5;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th5:
  G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J)
proof
  now
    let n;
    thus (G (#) H).n = H.n (#) G.n by Def7
      .= (H (#) G).n by Def7;
  end;
  hence G (#) H = H (#) G by FUNCT_2:63;
  now
    let n;
    thus ((G (#) H) (#) J).n = (G (#) H).n (#) J.n by Def7
      .= G.n (#) H.n (#) J.n by Def7
      .= G.n (#) (H.n (#) J.n) by RFUNCT_1:9
      .= G.n (#) (H (#) J).n by Def7
      .= (G (#) (H (#) J)).n by Def7;
  end;
  hence thesis by FUNCT_2:63;
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 Def7
      .= (G.n + H.n) (#) J.n by Def5
      .= G.n (#) J.n + H.n (#) J.n by RFUNCT_1:10
      .= (G(#)J).n + H.n (#) J.n by Def7
      .= (G(#)J).n + (H(#)J).n by Def7
      .= (G(#)J + H(#)J).n by Def5;
  end;
  hence (G + H) (#) J = G(#)J + H(#)J by FUNCT_2:63;
  hence J (#) (G + H) = G(#)J + H(#)J by Th5
    .= J(#)G + H(#)J by Th5
    .= J(#)G + J(#)H by Th5;
end;

theorem
  -H = (-1)(#)H
proof
  now
    let n;
    thus (-H).n = -H.n by Def3
      .=((-1)(#)H).n by Def1;
  end;
  hence thesis by FUNCT_2:63;
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 Def7
      .= (G.n - H.n) (#) J.n by Th3
      .= G.n (#) J.n - H.n (#) J.n by RFUNCT_1:14
      .= (G(#)J).n - H.n (#) J.n by Def7
      .= (G(#)J).n - (H(#)J).n by Def7
      .= (G(#)J - H(#)J).n by Th3;
  end;
  hence
A1: (G - H) (#) J = G(#)J - H(#)J by FUNCT_2:63;
  thus J(#)G - J(#)H = J(#)G - H(#)J by Th5
    .= (G - H) (#) J by A1,Th5
    .= J (#) (G - H) by Th5;
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 Def1
      .= r(#)(G.n + H.n) by Def5
      .= r(#)(G.n) + r(#)(H.n) by RFUNCT_1:16
      .=(r(#)G).n + r(#)(H.n) by Def1
      .=(r(#)G).n + (r(#)H).n by Def1
      .=(r(#)G + r(#)H).n by Def5;
  end;
  hence r(#)(G + H) = r(#)G + r(#)H by FUNCT_2:63;
  now
    let n;
    thus (r(#)(G - H)).n = r(#)(G - H).n by Def1
      .= r(#)(G.n - H.n) by Th3
      .= r(#)G.n - r(#)H.n by RFUNCT_1:18
      .= (r(#)G).n - r(#)H.n by Def1
      .= (r(#)G).n - (r(#)H).n by Def1
      .= (r(#)G - r(#)H).n by Th3;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  (r*p)(#)H = r(#)(p(#)H)
proof
  now
    let n;
    thus ((r*p)(#)H).n=(r*p)(#)H.n by Def1
      .=r(#)(p(#)H.n) by RFUNCT_1:17
      .=r(#)(p(#)H).n by Def1
      .=(r(#)(p(#)H)).n by Def1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  1 (#) H = H
proof
  now
    let n;
    thus (1 (#) H).n = 1 (#) H.n by Def1
      .= H.n by RFUNCT_1:21;
  end;
  hence thesis by FUNCT_2:63;
end;

canceled;

theorem
  G" (#) H" = (G(#)H)"
proof
  now
    let n;
    thus (G" (#) H").n = (G".n) (#) (H".n) by Def7
      .= ((G.n))^ (#) (H".n) by Def2
      .= ((G.n)^) (#) ((H.n)^) by Def2
      .= (G.n (#) H.n)^ by RFUNCT_1:27
      .= ((G (#) H).n)^ by Def7
      .= ((G (#) H)").n by Def2;
  end;
  hence thesis by FUNCT_2:63;
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 Def2
      .= (r (#) H.n)^ by Def1
      .= r" (#) ((H.n)^) by A1,RFUNCT_1:28
      .= r" (#) (H".n) by Def2
      .= (r" (#) H").n by Def1;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th15:
  abs(H)"=abs(H")
proof
  now
    let n;
    thus (abs(H")).n=abs(H".n) by Def4
      .=abs((H.n)^) by Def2
      .=(abs((H.n)))^ by RFUNCT_1:30
      .=(abs(H).n)^ by Def4
      .=(abs(H)").n by Def2;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th16:
  abs(G(#)H) = abs(G) (#) abs(H)
proof
  now
    let n;
    thus (abs(G(#)H)).n=abs(((G(#)H).n)) by Def4
      .=abs((G.n)(#)(H.n)) by Def7
      .=abs((G.n))(#)abs((H.n)) by RFUNCT_1:24
      .=((abs(G)).n)(#)abs((H.n)) by Def4
      .=((abs(G)).n)(#)(abs(H)).n by Def4
      .=(abs(G)(#)abs(H)).n by Def7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  abs(G/H) = abs(G) / abs(H)
proof
  thus abs(G/H)=abs(G)(#)abs((H")) by Th16
    .=abs(G)/abs(H) by Th15;
end;

theorem
  abs(r(#)H) = abs(r) (#) abs(H)
proof
  now
    let n;
    thus abs(r(#)H).n=abs((r(#)H).n) by Def4
      .=abs(r(#)(H.n)) by Def1
      .=abs(r)(#)abs(H.n) by RFUNCT_1:25
      .=abs(r)(#)(abs(H)).n by Def4
      .=(abs(r)(#)abs(H)).n by Def1;
  end;
  hence thesis by FUNCT_2:63;
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
  :Def9:
  X <> {} & for n holds X c= dom (F.n);
end;

definition
  let D,H,x;
  func H#x ->Real_Sequence means
  :Def10:
  for n holds it.n = (H.n).x;
  existence
  proof
    deffunc U(Element of NAT) = (H.$1).x;
    thus ex f being Real_Sequence st for n holds f.n = U(n) from SEQ_1:sch 1;
  end;
  uniqueness
  proof
    let S1,S2 such that
A1: for n holds S1.n = (H.n).x and
A2: for n holds S2.n = (H.n).x;
    now
      let n;
      S1.n = (H.n).x by A1;
      hence S1.n = S2.n by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let D,H,X;
  pred H is_point_conv_on X means
  :Def11:
  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 Th19:
  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 Def11;
    consider f such that
A2: X = dom f and
A3: 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,Def11;
    take f;
    thus X = dom f by A2;
    let x;
    assume
A4: x in X;
A5: now
      let p be real number;
      assume
A6:   p>0;
      p is Real by XREAL_0:def 1;
      then consider k such that
A7:   for n st n>=k holds abs((H.n).x - f.x) < p by A3,A4,A6;
      take k;
      let n;
      assume n>=k;
      then abs((H.n).x - f.x) < p by A7;
      hence abs((H#x).n - f.x) < p by Def10;
    end;
    hence (H#x) is convergent by SEQ_2:def 6;
    hence thesis by A5,SEQ_2:def 7;
  end;
  assume
A8: X common_on_dom H;
  given f such that
A9: X = dom f and
A10: 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 A9;
    let x;
    assume x in X;
    then
A11: (H#x) is convergent & lim(H#x) = f.x by A10;
    let p;
    assume p>0;
    then consider k such that
A12: for n st n>=k holds abs((H#x).n - f.x) < p by A11,SEQ_2:def 7;
    take k;
    let n;
    assume n >= k;
    then abs((H#x).n - f.x) < p by A12;
    hence thesis by Def10;
  end;
  hence thesis by A8,Def11;
end;

theorem Th20:
  H is_point_conv_on X iff X common_on_dom H & for x st x in X
  holds (H#x) is convergent
proof
  defpred X[set] means $1 in X;
  deffunc U(Element of D) = lim(H#$1);
  consider f such that
A1: for x holds x in dom f iff X[x] and
A2: for x st x in dom f holds f.x = U(x) from SEQ_1:sch 3;
  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
A3: H is_point_conv_on X;
    hence X common_on_dom H by Def11;
    let x;
    assume
A4: x in X;
    ex f st X = dom f & for x st x in X holds (H#x) is convergent & lim(H#
    x) = f.x by A3,Th19;
    hence thesis by A4;
  end;
  assume that
A5: X common_on_dom H and
A6: for x st x in X holds (H#x) is convergent;
  now
    take f;
    thus
A7: X = dom f
    proof
      thus X c= dom f
      proof
        let x be set such that
A8:     x in X;
        X c= dom (H.0) by A5,Def9;
        then X c= D by XBOOLE_1:1;
        then reconsider x9 = x as Element of D by A8;
        x9 in dom f by A1,A8;
        hence thesis;
      end;
      let x be set;
      assume x in dom f;
      hence thesis by A1;
    end;
    let x;
    assume
A9: x in X;
    hence (H#x) is convergent by A6;
    thus f.x = lim(H#x) by A2,A7,A9;
  end;
  hence thesis by A5,Th19;
end;

definition
  let D,H,X;
  pred H is_unif_conv_on X means
  :Def12:
  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
  :Def13:
  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 and
A3: for x st x in X holds (H#x) is convergent & lim(H#x) = f.x by A1,Th19;
    take f;
    thus dom f = X by A2;
    let x;
    assume x in dom f;
    hence thesis by A2,A3;
  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 SEQ_1:sch 4;
  end;
end;

theorem Th21:
  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,Def13;
    let x;
    assume
A4: x in X;
    then
A5: H#x is convergent by A1,Th20;
    let p;
    assume
A6: p>0;
    f.x = lim(H#x) by A1,A2,A3,A4,Def13;
    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 Def10;
  end;
  assume that
A8: dom f = X and
A9: 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
A10: x in dom f;
A11: now
      let p be real number;
      assume
A12:  p>0;
      p is Real by XREAL_0:def 1;
      then consider k such that
A13:  for n st n>=k holds abs((H.n).x - f.x) < p by A8,A9,A10,A12;
      take k;
      let n;
      assume n >= k;
      then abs((H.n).x - f.x) < p by A13;
      hence abs((H#x).n - f.x) < p by Def10;
    end;
    then H#x is convergent by SEQ_2:def 6;
    hence f.x = lim(H#x) by A11,SEQ_2:def 7;
  end;
  hence thesis by A1,A8,Def13;
end;

theorem Th22:
  H is_unif_conv_on X implies H is_point_conv_on X
proof
  assume
A1: H is_unif_conv_on X;
A2: now
    consider f such that
A3: X = dom f and
A4: 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,Def12;
    take f;
    thus X = dom f by A3;
    let x;
    assume
A5: x in X;
    let p;
    assume p>0;
    then consider k such that
A6: for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A4;
    take k;
    let n;
    assume n>=k;
    hence abs((H.n).x - f.x) < p by A5,A6;
  end;
  X common_on_dom H by A1,Def12;
  hence thesis by A2,Def11;
end;

theorem Th23:
  Y c= X & Y<>{} & X common_on_dom H implies Y common_on_dom H
proof
  assume that
A1: Y c= X and
A2: Y<>{} and
A3: X common_on_dom H;
  now
    let n;
    X c= dom (H.n) by A3,Def9;
    hence Y c= dom (H.n) by A1,XBOOLE_1:1;
  end;
  hence thesis by A2,Def9;
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 that
A1: Y c= X and
A2: Y<>{} and
A3: H is_point_conv_on X;
  consider f such that
A4: X = dom f and
A5: 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 A3,Def11;
A6: now
    take g = f|Y;
    thus
A7: Y = dom g by A1,A4,RELAT_1:62;
    let x;
    assume
A8: x in Y;
    let p;
    assume p>0;
    then consider k such that
A9: for n st n>=k holds abs((H.n).x - f.x) < p by A1,A5,A8;
    take k;
    let n;
    assume n>=k;
    then abs((H.n).x - f.x) < p by A9;
    hence abs((H.n).x - g.x) < p by A7,A8,FUNCT_1:47;
  end;
  X common_on_dom H by A3,Def11;
  then Y common_on_dom H by A1,A2,Th23;
  hence
A10: H is_point_conv_on Y by A6,Def11;
A11: now
    let x;
    assume
A12: x in dom (lim(H,X)|Y);
    then
A13: x in (dom lim(H,X)) /\ Y by RELAT_1:61;
    then
A14: x in dom lim(H,X) by XBOOLE_0:def 4;
    x in Y by A13,XBOOLE_0:def 4;
    then
A15: x in dom lim(H,Y) by A10,Def13;
    thus (lim(H,X)|Y).x = (lim(H,X)).x by A12,FUNCT_1:47
      .= lim (H#x) by A3,A14,Def13
      .= (lim(H,Y)).x by A10,A15,Def13;
  end;
  dom lim(H,X) = X by A3,Def13;
  then dom lim(H,X) /\ Y = Y by A1,XBOOLE_1:28;
  then dom (lim(H,X)|Y) = Y by RELAT_1:61;
  then dom (lim(H,X)|Y) = dom lim(H,Y) by A10,Def13;
  hence thesis by A11,PARTFUN1:5;
end;

theorem
  Y c= X & Y<>{} & H is_unif_conv_on X implies H is_unif_conv_on Y
proof
  assume that
A1: Y c= X and
A2: Y<>{} and
A3: H is_unif_conv_on X;
  consider f such that
A4: dom f = X and
A5: 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 A3,Def12;
A6: now
    take g = f|Y;
    thus
A7: dom g = dom f /\ Y by RELAT_1:61
      .= Y by A1,A4,XBOOLE_1:28;
    let p;
    assume p>0;
    then consider k such that
A8: for n,x st n>=k & x in X holds abs((H.n).x - f.x) < p by A5;
    take k;
    let n,x;
    assume that
A9: n>=k and
A10: x in Y;
    abs((H.n).x - f.x) < p by A1,A8,A9,A10;
    hence abs((H.n).x - g.x) < p by A7,A10,FUNCT_1:47;
  end;
  X common_on_dom H by A3,Def12;
  then Y common_on_dom H by A1,A2,Th23;
  hence thesis by A6,Def12;
end;

theorem Th26:
  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} <> {};
  now
    let n;
    X c= dom(H.n) by A1,Def9;
    hence {x} c= dom(H.n) by A2,ZFMISC_1:31;
  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 Def11;
  hence thesis by Th26;
end;

theorem Th28:
  {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 that
A1: {x} common_on_dom H1 and
A2: {x} common_on_dom H2;
  now
    let n;
A3: {x} c= dom (H2.n) by A2,Def9;
    x in {x} & {x} c= dom(H1.n) by A1,Def9,TARSKI:def 1;
    then x in (dom(H1.n) /\ dom(H2.n)) by A3,XBOOLE_0:def 4;
    then
A4: x in dom(H1.n + H2.n) by VALUED_1:def 1;
    thus (H1#x + H2#x).n = (H1#x).n + (H2#x).n by SEQ_1:7
      .= (H1.n).x + (H2#x).n by Def10
      .= (H1.n).x + (H2.n).x by Def10
      .= ((H1.n) + (H2.n)).x by A4,VALUED_1:def 1
      .= ((H1+H2).n).x by Def5
      .= ((H1+H2)#x).n by Def10;
  end;
  hence H1#x + H2#x = (H1+H2)#x by FUNCT_2:63;
  now
    let n;
A5: {x} c= dom (H2.n) by A2,Def9;
    x in {x} & {x} c= dom(H1.n) by A1,Def9,TARSKI:def 1;
    then x in (dom(H1.n) /\ dom(H2.n)) by A5,XBOOLE_0:def 4;
    then
A6: x in dom(H1.n - H2.n) by VALUED_1:12;
    thus (H1#x - H2#x).n = (H1#x).n - (H2#x).n by RFUNCT_2:1
      .= (H1.n).x - (H2#x).n by Def10
      .= (H1.n).x - (H2.n).x by Def10
      .= ((H1.n) - (H2.n)).x by A6,VALUED_1:13
      .= ((H1-H2).n).x by Th3
      .= ((H1-H2)#x).n by Def10;
  end;
  hence H1#x - H2#x = (H1-H2)#x by FUNCT_2:63;
  now
    let n;
    thus ((H1#x) (#) (H2#x)).n = (H1#x).n * (H2#x).n by SEQ_1:8
      .= (H1.n).x * (H2#x).n by Def10
      .= (H1.n).x * (H2.n).x by Def10
      .= ((H1.n) (#) (H2.n)).x by VALUED_1:5
      .= ((H1(#)H2).n).x by Def7
      .= ((H1(#)H2)#x).n by Def10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th29:
  (abs(H))#x = abs(H#x) & (-H)#x = -(H#x)
proof
  now
    let n;
    thus ((abs(H))#x).n = (abs(H).n).x by Def10
      .= abs((H.n)).x by Def4
      .= abs((H.n).x) by VALUED_1:18
      .= abs((H#x).n) by Def10
      .= abs((H#x)).n by SEQ_1:12;
  end;
  hence (abs(H))#x = abs((H#x)) by FUNCT_2:63;
  now
    let n;
    thus ((-H)#x).n = ((-H).n).x by Def10
      .= (-H.n).x by Def3
      .= -((H.n).x) by VALUED_1:8
      .= -((H#x).n) by Def10
      .= (-(H#x)).n by SEQ_1:10;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th30:
  {x} common_on_dom H implies (r(#)H)#x = r(#)(H#x)
proof
  assume
A1: {x} common_on_dom H;
  now
    let n;
    x in {x} & {x} c= dom(H.n) by A1,Def9,TARSKI:def 1;
    then x in dom (H.n);
    then
A2: x in dom (r(#)(H.n)) by VALUED_1:def 5;
    thus ((r(#)H)#x).n = ((r(#)H).n).x by Def10
      .= (r(#)(H.n)).x by Def1
      .= r*((H.n).x) by A2,VALUED_1:def 5
      .= r*((H#x).n) by Def10
      .= (r(#)(H#x)).n by SEQ_1:9;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem Th31:
  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 x in X;
  then {x} common_on_dom H1 & {x} common_on_dom H2 by A1,Th26;
  hence thesis by Th28;
end;

theorem Th32:
  abs(H)#x = abs(H#x) & (-H)#x = -(H#x) by Th29;

theorem Th33:
  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,Th26;
  hence thesis by Th30;
end;

theorem Th34:
  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 H1 is_point_conv_on X & H2 is_point_conv_on X;
  then X common_on_dom H1 & X common_on_dom H2 by Def11;
  hence thesis by Th31;
end;

theorem
  abs(H)#x = abs(H#x) & (-H)#x = -(H#x) by Th32;

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 Def11;
  hence thesis by Th33;
end;

theorem Th37:
  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 that
A1: X common_on_dom H1 and
A2: X common_on_dom H2;
A3: X <> {} by A1,Def9;
  now
    let n;
    X c= dom (H1.n) & X c= dom (H2.n) by A1,A2,Def9;
    then X c= dom (H1.n) /\ dom (H2.n) by XBOOLE_1:19;
    then X c= dom (H1.n + H2.n) by VALUED_1:def 1;
    hence X c= dom ((H1+H2).n) by Def5;
  end;
  hence X common_on_dom H1+H2 by A3,Def9;
  now
    let n;
    X c= dom (H1.n) & X c= dom (H2.n) by A1,A2,Def9;
    then X c= dom (H1.n) /\ dom (H2.n) by XBOOLE_1:19;
    then X c= dom (H1.n - H2.n) by VALUED_1:12;
    hence X c= dom ((H1-H2).n) by Th3;
  end;
  hence X common_on_dom H1-H2 by A3,Def9;
  now
    let n;
    X c= dom (H1.n) & X c= dom (H2.n) by A1,A2,Def9;
    then X c= dom (H1.n) /\ dom (H2.n) by XBOOLE_1:19;
    then X c= dom (H1.n (#) H2.n) by VALUED_1:def 4;
    hence X c= dom ((H1(#)H2).n) by Def7;
  end;
  hence thesis by A3,Def9;
end;

theorem Th38:
  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 Def9;
  now
    let n;
    dom (H.n) = dom (abs(H.n)) by VALUED_1:def 11
      .= dom (abs(H).n) by Def4;
    hence X c= dom (abs(H).n) by A1,Def9;
  end;
  hence X common_on_dom abs(H) by A2,Def9;
  now
    let n;
    dom (H.n) = dom (-(H.n)) by VALUED_1:8
      .= dom ((-H).n) by Def3;
    hence X c= dom ((-H).n) by A1,Def9;
  end;
  hence thesis by A2,Def9;
end;

theorem Th39:
  X common_on_dom H implies X common_on_dom r(#)H
proof
  assume
A1: X common_on_dom H;
A2: now
    let n;
    dom (H.n) = dom(r(#)(H.n)) by VALUED_1:def 5
      .= dom ((r(#)H).n) by Def1;
    hence X c= dom ((r(#)H).n) by A1,Def9;
  end;
  X <> {} by A1,Def9;
  hence thesis by A2,Def9;
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 that
A1: H1 is_point_conv_on X and
A2: H2 is_point_conv_on X;
A3: now
    let x;
    assume
A4: x in X;
    then H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    then (H1#x)+(H2#x) is convergent by SEQ_2:5;
    hence (H1+H2)#x is convergent by A1,A2,A4,Th34;
  end;
A5: now
    let x;
    assume
A6: x in X;
    then H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    then (H1#x)-(H2#x) is convergent by SEQ_2:11;
    hence (H1-H2)#x is convergent by A1,A2,A6,Th34;
  end;
A7: X common_on_dom H1 & X common_on_dom H2 by A1,A2,Th20;
  then X common_on_dom H1+H2 by Th37;
  hence
A8: H1+H2 is_point_conv_on X by A3,Th20;
A9: now
    let x;
    assume
A10: x in dom (lim(H1,X)+lim(H2,X));
    then
A11: x in (dom lim(H1,X))/\(dom lim(H2,X)) by VALUED_1:def 1;
    then
A12: x in (dom lim(H2,X)) by XBOOLE_0:def 4;
A13: x in (dom lim(H1,X)) by A11,XBOOLE_0:def 4;
    then
A14: x in X by A1,Def13;
    then
A15: H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    thus (lim(H1,X) + lim(H2,X)).x = (lim(H1,X)).x + (lim(H2,X)).x by A10,
VALUED_1:def 1
      .= lim(H1#x) + (lim(H2,X)).x by A1,A13,Def13
      .= lim(H1#x) + lim(H2#x) by A2,A12,Def13
      .= lim((H1#x) + (H2#x)) by A15,SEQ_2:6
      .= lim((H1+H2)#x) by A1,A2,A14,Th34;
  end;
A16: now
    let x;
    assume
A17: x in X;
    then H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    then (H1#x)(#)(H2#x) is convergent by SEQ_2:14;
    hence (H1(#)H2)#x is convergent by A1,A2,A17,Th34;
  end;
A18: now
    let x;
    assume x in dom (lim(H1,X)(#)lim(H2,X));
    then
A19: x in (dom lim(H1,X))/\(dom lim(H2,X)) by VALUED_1:def 4;
    then
A20: x in (dom lim(H2,X)) by XBOOLE_0:def 4;
A21: x in (dom lim(H1,X)) by A19,XBOOLE_0:def 4;
    then
A22: x in X by A1,Def13;
    then
A23: H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    thus (lim(H1,X) (#) lim(H2,X)).x = (lim(H1,X)).x * (lim(H2,X)).x by
VALUED_1:5
      .= lim(H1#x) * (lim(H2,X)).x by A1,A21,Def13
      .= lim(H1#x) * lim(H2#x) by A2,A20,Def13
      .= lim((H1#x) (#) (H2#x)) by A23,SEQ_2:15
      .= lim((H1(#)H2)#x) by A1,A2,A22,Th34;
  end;
A24: now
    let x;
    assume
A25: x in dom (lim(H1,X)-lim(H2,X));
    then
A26: x in (dom lim(H1,X))/\(dom lim(H2,X)) by VALUED_1:12;
    then
A27: x in (dom lim(H2,X)) by XBOOLE_0:def 4;
A28: x in (dom lim(H1,X)) by A26,XBOOLE_0:def 4;
    then
A29: x in X by A1,Def13;
    then
A30: H1#x is convergent & H2#x is convergent by A1,A2,Th20;
    thus (lim(H1,X) - lim(H2,X)).x = (lim(H1,X)).x - (lim(H2,X)).x by A25,
VALUED_1:13
      .= lim(H1#x) - (lim(H2,X)).x by A1,A28,Def13
      .= lim(H1#x) - lim(H2#x) by A2,A27,Def13
      .= lim((H1#x) - (H2#x)) by A30,SEQ_2:12
      .= lim((H1-H2)#x) by A1,A2,A29,Th34;
  end;
  dom (lim(H1,X)+lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by
VALUED_1:def 1
    .= X /\ (dom lim(H2,X)) by A1,Def13
    .= X /\ X by A2,Def13
    .= X;
  hence lim(H1+H2,X) = lim(H1,X) + lim(H2,X) by A8,A9,Def13;
  X common_on_dom H1-H2 by A7,Th37;
  hence
A31: H1-H2 is_point_conv_on X by A5,Th20;
  dom (lim(H1,X)-lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by VALUED_1:12
    .= X /\ (dom lim(H2,X)) by A1,Def13
    .= X /\ X by A2,Def13
    .= X;
  hence lim(H1-H2,X) = lim(H1,X) - lim(H2,X) by A31,A24,Def13;
  X common_on_dom H1 (#)H2 by A7,Th37;
  hence
A32: H1(#)H2 is_point_conv_on X by A16,Th20;
  dom (lim(H1,X)(#)lim(H2,X))=(dom lim(H1,X)) /\ (dom lim(H2,X)) by
VALUED_1:def 4
    .= X /\ (dom lim(H2,X)) by A1,Def13
    .= X /\ X by A2,Def13
    .= X;
  hence thesis by A32,A18,Def13;
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;
A2: now
    let x;
    assume x in X;
    then H#x is convergent by A1,Th20;
    then abs(H#x) is convergent by SEQ_4:13;
    hence abs(H)#x is convergent by Th32;
  end;
A3: now
    let x;
    assume x in dom (-lim(H,X));
    then
A4: x in dom lim(H,X) by VALUED_1:8;
    then x in X by A1,Def13;
    then
A5: H#x is convergent by A1,Th20;
    thus (-lim(H,X)).x = -(lim(H,X).x) by VALUED_1:8
      .= -(lim(H#x)) by A1,A4,Def13
      .= lim(-(H#x)) by A5,SEQ_2:10
      .= lim((-H)#x) by Th32;
  end;
A6: X common_on_dom H by A1,Th20;
  then X common_on_dom abs(H) by Th38;
  hence
A7: abs(H) is_point_conv_on X by A2,Th20;
A8: now
    let x;
    assume x in dom abs(lim(H,X));
    then
A9: x in dom lim(H,X) by VALUED_1:def 11;
    then x in X by A1,Def13;
    then
A10: H#x is convergent by A1,Th20;
    thus abs(lim(H,X)).x = abs(lim(H,X).x) by VALUED_1:18
      .= abs(lim(H#x)) by A1,A9,Def13
      .= lim abs((H#x)) by A10,SEQ_4:14
      .= lim(abs(H)#x) by Th32;
  end;
A11: now
    let x;
    assume x in X;
    then H#x is convergent by A1,Th20;
    then -(H#x) is convergent by SEQ_2:9;
    hence (-H)#x is convergent by Th32;
  end;
  dom abs(lim(H,X)) = dom lim(H,X) by VALUED_1:def 11
    .= X by A1,Def13;
  hence lim (abs(H),X) = abs( lim (H,X) ) by A7,A8,Def13;
  X common_on_dom -H by A6,Th38;
  hence
A12: -H is_point_conv_on X by A11,Th20;
  dom (-lim(H,X)) = dom lim(H,X) by VALUED_1:8
    .= X by A1,Def13;
  hence thesis by A12,A3,Def13;
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 by Th20;
A3: now
    let x;
    assume
A4: x in dom(r(#)(lim(H,X)));
    then
A5: x in dom lim(H,X) by VALUED_1:def 5;
    then
A6: x in X by A1,Def13;
    then
A7: H#x is convergent by A1,Th20;
    thus (r(#)lim(H,X)).x = r*(lim(H,X).x) by A4,VALUED_1:def 5
      .= r*(lim(H#x)) by A1,A5,Def13
      .= lim(r(#)(H#x)) by A7,SEQ_2:8
      .= lim((r(#)H)#x) by A2,A6,Th33;
  end;
A8: now
    let x;
    assume
A9: x in X;
    then H#x is convergent by A1,Th20;
    then r(#)(H#x) is convergent by SEQ_2:7;
    hence (r(#)H)#x is convergent by A2,A9,Th33;
  end;
  X common_on_dom r(#)H by A2,Th39;
  hence
A10: r(#)H is_point_conv_on X by A8,Th20;
  dom(r(#)(lim(H,X))) = dom lim(H,X) by VALUED_1:def 5
    .= X by A1,Def13;
  hence thesis by A10,A3,Def13;
end;

theorem Th43:
  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 and
A3: 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 Def12;
    thus X common_on_dom H by A1,Def12;
A4: now
      let x such that
A5:   x in X;
      let p;
      assume p>0;
      then consider k such that
A6:   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 A5,A6;
    end;
    thus H is_point_conv_on X by A1,Th22;
    then
A7: f = (lim(H,X)) by A2,A4,Th21;
    let r;
    assume r > 0;
    then consider k such that
A8: for n,x st n>=k & x in X holds abs((H.n).x-f.x)<r by A3;
    take k;
    let n,x;
    assume n>=k & x in X;
    hence thesis by A7,A8;
  end;
  assume that
A9: X common_on_dom H and
A10: H is_point_conv_on X and
A11: 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;
  dom lim(H,X) = X by A10,Def13;
  hence thesis by A9,A11,Def12;
end;

reserve H for Functional_Sequence of REAL,REAL;

theorem
  H is_unif_conv_on X & (for n holds (H.n)|X is continuous) implies lim(
  H,X)|X is continuous
proof
  set l = lim(H,X);
  assume that
A1: H is_unif_conv_on X and
A2: for n holds (H.n)|X is continuous;
A3: H is_point_conv_on X by A1,Th22;
  then
A4: dom l = X by Def13;
A5: X common_on_dom H by A1,Def12;
  for x0 be real number st x0 in dom(l|X) holds l|X is_continuous_in x0
  proof
    let x0 be real number;
    assume x0 in dom(l|X);
    then
A6: x0 in X by RELAT_1:57;
    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 XREAL_1:222;
      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,Th43;
      consider k1 be Element of NAT such that
A9:   for n st n>=k1 holds abs((H.n).x0 - l.x0) < r/3 by A3,A6,A7,Th21;
      set m = max(k,k1);
      set h = H.m;
A10:  X c= dom h by A5,Def9;
A11:  dom(h|X) = dom h /\ X by RELAT_1:61
        .= X by A10,XBOOLE_1:28;
      h|X is continuous by A2;
      then h|X is_continuous_in x0 by A6,A11,FCONT_1:def 2;
      then consider s be real number such that
A12:  0<s and
A13:  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 A12;
      let x1 be real number;
      assume that
A14:  x1 in dom (l|X) and
A15:  abs(x1-x0)<s;
A16:  dom (l|X) = dom l /\ X by RELAT_1:61
        .= X by A4;
      then abs((h|X).x1-(h|X).x0)<r/3 by A11,A13,A14,A15;
      then abs(h.x1-(h|X).x0)<r/3 by A16,A11,A14,FUNCT_1:47;
      then
A17:  abs(h.x1-h.x0)<r/3 by A6,FUNCT_1:49;
      abs(h.x0 - l.x0) < r/3 by A9,XXREAL_0:25;
      then
      abs((h.x1-h.x0)+(h.x0-l.x0))<=abs(h.x1-h.x0)+abs(h.x0-l.x0) & abs(h
      .x1-h.x0) +abs(h.x0-l.x0) < r/3 + r/3 by A17,COMPLEX1:56,XREAL_1:8;
      then
A18:  abs((h.x1-h.x0)+(h.x0-l.x0))<r/3+r/3 by XXREAL_0:2;
      abs(l.x1 - l.x0) = abs((l.x1-h.x1)+((h.x1-h.x0)+(h.x0-l.x0)));
      then
A19:  abs(l.x1 - l.x0) <= abs(l.x1-h.x1)+ abs((h.x1-h.x0)+(h.x0-l.x0 ) )
      by COMPLEX1:56;
      abs(h.x1-l.x1)<r/3 by A8,A16,A14,XXREAL_0:25;
      then abs(-(l.x1-h.x1))<r/3;
      then abs(l.x1-h.x1)<r/3 by COMPLEX1:52;
      then abs(l.x1-h.x1)+ abs((h.x1-h.x0)+(h.x0-l.x0)) < r/3 +(r/3+r/3) by A18
,XREAL_1:8;
      then abs(l.x1 - l.x0) < r/3 +r/3+r/3 by A19,XXREAL_0:2;
      then abs((l|X).x1 - l.x0) < r by A14,FUNCT_1:47;
      hence thesis by A4,RELAT_1:68;
    end;
    hence thesis by FCONT_1:3;
  end;
  hence thesis by FCONT_1:def 2;
end;