Copyright (c) 1992 Association of Mizar Users
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;