:: Conjugate Sequences, Bounded Complex Sequences and Convergent
:: Complex Sequences
:: by Adam Naumowicz
::
:: Received December 20, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, COMSEQ_1, COMPLEX1, RELAT_1, ARYTM_1,
ARYTM_3, CARD_1, XXREAL_0, FUNCT_1, XBOOLE_0, PARTFUN1, VALUED_0,
VALUED_1, XXREAL_2, FUNCOP_1, SEQ_2, ORDINAL2, XCMPLX_0, PBOOLE, TARSKI,
NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, RELAT_1, REAL_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2,
FUNCOP_1, VALUED_0, VALUED_1, NAT_1, COMSEQ_1, XXREAL_0;
constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1,
RELSET_1, PBOOLE, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, VALUED_1, VALUED_0, XCMPLX_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RELAT_1, FUNCT_1, PARTFUN1;
equalities VALUED_1;
theorems COMSEQ_1, COMPLEX1, NAT_1, FUNCT_2, XREAL_0, XCMPLX_0, XCMPLX_1,
FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, PARTFUN1, VALUED_0, ORDINAL1,
NUMBERS;
schemes NAT_1, FUNCT_1;
begin :: Preliminaries
reserve n,n1,n2,m for Nat;
reserve r,g1,g2,g,g9 for Complex;
reserve R,R2 for Real;
reserve s,s9,s1 for Complex_Sequence;
theorem Th1:
g<>0c & r<>0c implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|)
proof
assume
A1: g<>0c & r<>0c;
thus |.g"-r".|=|.1r/g-r".| by COMPLEX1:def 4,XCMPLX_1:215
.=|.1r/g-1r/r.| by COMPLEX1:def 4,XCMPLX_1:215
.=|.1r/g+-1r/r.|
.=|.1r/g+-1r*r".| by XCMPLX_0:def 9
.=|.1r/g+(-1r)*r".|
.=|.1r/g+(-1r)/r.| by XCMPLX_0:def 9
.=|.(1r*r+(-1r)*g)/(r*g).| by A1,XCMPLX_1:116
.=|.r-g.|/|.g*r.| by COMPLEX1:67,def 4
.=|.-(g-r).|/(|.g.|*|.r.|) by COMPLEX1:65
.=|.g-r.|/(|.g.|*|.r.|) by COMPLEX1:52;
end;
theorem Th2:
for n ex r being Real st 0<r & for m st m<=n holds |.s.m.|<r
proof
let n;
defpred P[Nat] means
ex r being Real st 0<r & for m st m<= $1 holds |.s.m.|<r;
A1: for n st P[n] holds P[n+1]
proof
let n;
given R1 be Real such that
A2: 0<R1 and
A3: for m st m <= n holds |.s.m.| < R1;
A4: now
assume
A5: R1 <= |.s.(n+1).|;
take R= |.s.(n+1).| +1;
0+0<R by COMPLEX1:46,XREAL_1:8;
hence 0<R;
let m such that
A6: m<=n+1;
A7: now
assume m<=n;
then |.s.m.| <R1 by A3;
then |.s.m.| < |.s.(n+1).| by A5,XXREAL_0:2;
then |.s.m.| + 0 < R by XREAL_1:8;
hence |.s.m.| < R;
end;
now
assume m=n+1;
then |.s.m.| +0 <R by XREAL_1:8;
hence |.s.m.| < R;
end;
hence |.s.m.| <R by A6,A7,NAT_1:8;
end;
now
assume
A8: |.s.(n+1).| <= R1;
take R=R1+1;
thus R>0 by A2;
let m such that
A9: m <= n+1;
A10: now
assume m <= n;
then
A11: |.s.m.| < R1 by A3;
R1+0<R by XREAL_1:8;
hence |.s.m.| < R by A11,XXREAL_0:2;
end;
now
A12: R1+0 <R by XREAL_1:8;
assume m=n+1;
hence |.s.m.| < R by A8,A12,XXREAL_0:2;
end;
hence |.s.m.| < R by A9,A10,NAT_1:8;
end;
hence thesis by A4;
end;
A13: P[0]
proof
take R=|.s.0.|+1;
0+0 < |.s.0.| +1 by COMPLEX1:46,XREAL_1:8;
hence 0<R;
let m;
assume m <= 0;
then m=0;
then |.s.m.| +0 < R by XREAL_1:8;
hence thesis;
end;
for n holds P[n] from NAT_1:sch 2(A13,A1);
then consider R being Real such that
A14: R>0 & for m st m<=n holds |.s.m.|<R;
thus thesis by A14;
end;
begin :: Conjugate Sequences
definition
let f be complex-valued Function;
deffunc F(object) = (f.$1)*';
func f*' -> complex-valued Function means
:Def1:
dom it = dom f &
for c being set st c in dom it holds it.c = (f.c)*';
existence
proof
consider F being Function such that
A1: dom F = dom f and
A2: for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3;
for x being object st x in dom F holds F.x is complex
proof let x be object;
assume x in dom F;
then F.x = F(x) by A1,A2;
hence thesis;
end;
then reconsider F as complex-valued Function by VALUED_0:def 7;
take F;
thus dom f = dom F by A1;
thus thesis by A1,A2;
end;
uniqueness
proof
let h,g be complex-valued Function such that
A3: dom h=dom f and
A4: for c be set st c in dom h holds h.c = F(c) and
A5: dom g=dom f and
A6: for c be set st c in dom g holds g.c = F(c);
thus dom h=dom g by A3,A5;
let x be object;
assume
A7: x in dom h;
hence h.x = F(x) by A4
.= g.x by A3,A5,A6,A7;
end;
involutiveness
proof let g,f be complex-valued Function;
assume that
A8: dom g = dom f and
A9: for c being set st c in dom g holds g.c = (f.c)*';
thus dom f = dom g by A8;
let c be set;
assume
A10: c in dom f;
thus f.c = (f.c)*'*'
.= (g.c)*' by A8,A10,A9;
end;
end;
definition
let C be non empty set;
let f be Function of C,COMPLEX;
redefine func f*' -> Function of C,COMPLEX means :: redefines *' (COMSEQ_2, definition)
:Def2:
for n being Element of C holds it.n=(f.n)*';
coherence
proof
A1: dom(f*') = dom f by Def1
.= C by PARTFUN1:def 2;
for x being object st x in C holds (f*').x in COMPLEX by XCMPLX_0:def 2;
hence f*' is Function of C,COMPLEX by A1,FUNCT_2:3;
end;
compatibility
proof
let IT be Function of C,COMPLEX;
A2: dom IT = C by FUNCT_2:def 1;
hence IT = f*' implies for c being Element of C holds IT.c = (f.c)*'
by Def1;
assume
A3: for c being Element of C holds IT.c = (f.c)*';
A4: dom IT = dom f by A2,FUNCT_2:def 1;
for c being set st c in dom IT holds IT.c = (f.c)*' by A3;
hence IT = f*' by A4,Def1;
end;
end;
registration
let C be non empty set;
let s be complex-valued ManySortedSet of C;
cluster s*' -> C-defined;
coherence
proof
dom s c= C;
hence dom(s*') c= C by Def1;
end;
end;
registration
let C be non empty set;
let seq be complex-valued ManySortedSet of C;
cluster seq*' -> total for C-defined Function;
coherence
proof let f be C-defined Function;
assume f = seq*';
hence dom f = dom seq by Def1
.= C by PARTFUN1:def 2;
end;
end;
theorem
s is non-zero implies s*' is non-zero
proof
assume
A1: s is non-zero;
now
let n be Element of NAT;
s.n <> 0 by A1,COMSEQ_1:3;
then (s.n)*' <>0c by COMPLEX1:29;
hence s*'.n <>0c by Def2;
end;
hence thesis by COMSEQ_1:4;
end;
theorem
(r(#)s)*' = (r*')(#)(s*')
proof
now
let n be Element of NAT;
thus (r(#)s)*'.n = ((r(#)s).n)*' by Def2
.= (r*s.n)*' by VALUED_1:6
.= (r*')*(s.n)*' by COMPLEX1:35
.= (r*')*(s*'.n) by Def2
.= ((r*')(#)(s*')).n by VALUED_1:6;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(s (#) s9)*' = (s*') (#) (s9*')
proof
now
let n be Element of NAT;
thus (s (#) s9)*'.n = ((s (#) s9).n)*' by Def2
.= (s.n * s9.n)*' by VALUED_1:5
.= (s.n)*' * (s9.n)*' by COMPLEX1:35
.= (s*'.n) * (s9.n)*' by Def2
.= (s*'.n) * (s9*'.n) by Def2
.= (s*' (#) s9*').n by VALUED_1:5;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(s*')" = (s")*'
proof
now
let n be Element of NAT;
thus (s*')".n = (s*'.n)" by VALUED_1:10
.= ((s.n)*')" by Def2
.= ((s.n)")*' by COMPLEX1:36
.= (s".n)*' by VALUED_1:10
.= (s")*'.n by Def2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(s9/"s)*' = (s9*') /" (s*')
proof
now
let n be Element of NAT;
thus (s9/"s)*'.n = ((s9 (#) s").n)*' by Def2
.= ((s9.n) * (s".n))*' by VALUED_1:5
.= ((s9.n) * (s.n)")*' by VALUED_1:10
.= (s9.n)*' * ((s.n)")*' by COMPLEX1:35
.= (s9.n)*' * ((s.n)*')" by COMPLEX1:36
.= (s9*').n * ((s.n)*')" by Def2
.= (s9*').n * ((s*').n)" by Def2
.= (s9*').n * ((s*')").n by VALUED_1:10
.= ((s9*') /" (s*')).n by VALUED_1:5;
end;
hence thesis by FUNCT_2:63;
end;
begin :: BOUNDED COMPLEX SEQUENCES
definition
let f be complex-valued Function;
attr f is bounded means
:: SEQ_2:def 5
ex r being Real st
for y being set st y in dom f holds |.f.y.| <r;
end;
definition
let s;
redefine attr s is bounded means :: redefines bounded (COMSEQ_2, definition)
ex r being Real st for n holds |.s.n .|<r;
compatibility
proof
thus s is bounded implies ex r being Real st for n holds |.s.n.|<r
proof
given r being Real such that
A1: for y being set st y in dom s holds |.s.y.| < r;
reconsider r as Element of REAL by XREAL_0:def 1;
take r;
let n;
n in NAT by ORDINAL1:def 12;
then n in dom s by FUNCT_2:def 1;
hence thesis by A1;
end;
given r being Real such that
A2: for n holds |.s.n.|<r;
take r;
let y being set;
assume y in dom s;
hence thesis by A2;
end;
end;
set sc = NAT --> 0c;
registration
cluster bounded for Complex_Sequence;
existence
proof
1 in NAT;
then reconsider j = 1 as Element of REAL by NUMBERS:19;
take sc, j;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by COMPLEX1:44,FUNCOP_1:7;
end;
end;
theorem Th8:
s is bounded iff ex r being Real st (0<r & for n holds |.s.n.|<r)
proof
thus s is bounded implies
ex r being Real st (0<r & for n holds |.s.n.|<r)
proof
assume s is bounded;
then consider r being Real such that
A1: for n holds |.s.n.|<r;
take r;
now
let n;
0 <= |.s.n.| by COMPLEX1:46;
hence 0< r by A1;
end;
hence thesis by A1;
end;
thus thesis;
end;
begin
:: Convergent Complex Sequences
:: The Limit of Complex Sequences
definition
let s be complex-valued ManySortedSet of NAT;
attr s is convergent means
:Def5:
ex g st for p be Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<p;
end;
definition
let s;
assume
A1: s is convergent;
func lim s -> Complex means
:Def6:
for p be Real st 0<p ex n st for m st n<=m holds |.s.m-it.|<p;
existence by A1;
uniqueness
proof
let g1,g2;
assume that
A2: for p be Real st 0<p ex n1 st for m st n1<=m holds |.s.m-g1.|<p and
A3: for p be Real st 0<p ex n2 st for m st n2<=m holds |.s.m-g2.|<p and
A4: g1<>g2;
reconsider p = |.g1 - g2.|/2 as Real;
A5: |.g1-g2.| > 0 by A4,COMPLEX1:62;
then consider n1 such that
A6: for m st n1<=m holds |.s.m-g1.|<p by A2;
consider n2 such that
A7: for m st n2<=m holds |.s.m-g2.|<p by A3,A5;
reconsider n = max(n1,n2) as Element of NAT by ORDINAL1:def 12;
for m st n <= m holds 2*p<2*p
proof
let m;
assume
A8: n <= m;
n2<=n by XXREAL_0:25;
then n + n2 <= n + m by A8,XREAL_1:7;
then n2<=m by XREAL_1:6;
then
A9: |.s.m - g2.|< p by A7;
|.g1 - g2.| = |.g1 - s.m - (g2 - s.m).|;
then |.g1 - g2.| <= |.g1-s.m.| + |.g2-s.m.| by COMPLEX1:57;
then
A10: |.g1 - g2.| <= |.s.m - g1.| + |.g2-s.m.| by COMPLEX1:60;
n1<=n by XXREAL_0:25;
then n + n1 <= n + m by A8,XREAL_1:7;
then n1<=m by XREAL_1:6;
then |.s.m - g1.|< p by A6;
then |.s.m - g1.| + |.s.m - g2.| <p + p by A9,XREAL_1:8;
hence thesis by A10,COMPLEX1:60;
end;
hence contradiction;
end;
end;
theorem Th9:
(ex g st for n being Nat holds s.n = g) implies s is convergent
proof
reconsider zz=0 as Nat;
given g such that
A1: for n being Nat holds s.n = g;
take g;
now
let p be Real such that
A2: 0<p;
take k = zz;
let n such that
k<=n;
s.n = g by A1;
hence |.s.n - g.| < p by A2,COMPLEX1:44;
end;
hence thesis;
end;
theorem Th10:
for g st for n being Nat holds s.n = g holds lim s = g
proof
let g;
assume
A1: for n being Nat holds s.n = g;
A2: now
let p be Real such that
A3: 0<p;
reconsider zz=0 as Nat;
take k = zz;
let n such that
k<=n;
s.n = g by A1;
hence |.s.n - g.| < p by A3,COMPLEX1:44;
end;
s is convergent by A1,Th9;
hence thesis by A2,Def6;
end;
registration
cluster convergent for Complex_Sequence;
existence
proof
for n being Nat holds sc.n = 0c
by ORDINAL1:def 12,FUNCOP_1:7;
hence thesis by Th9;
end;
end;
registration
let s be convergent Complex_Sequence;
cluster s*' -> convergent for Complex_Sequence;
coherence
proof let t be Complex_Sequence such that
A1: t = s*';
consider g such that
A2: for p being Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<p
by Def5;
reconsider z = g*' as Element of COMPLEX by XCMPLX_0:def 2;
take r = z;
let p be Real;
assume 0<p;
then consider n such that
A3: for m st n<=m holds |.s.m-g.|<p by A2;
take n;
let m such that
A4: n<=m;
m in NAT by ORDINAL1:def 12;
then |.(s*').m - r.| = |.(s.m)*' - g*'.| by Def2
.= |.(s.m - g)*'.| by COMPLEX1:34
.= |.s.m-g.| by COMPLEX1:53;
hence thesis by A3,A4,A1;
end;
end;
::$CT
theorem Th11:
s is convergent implies lim(s*') = (lim s)*'
proof
set g = lim s;
assume
A1: s is convergent;
then reconsider s1 = s as convergent Complex_Sequence;
A2: now
let p be Real;
assume 0<p;
then consider n such that
A3: for m st n<=m holds |.s.m-g.|<p by A1,Def6;
take n;
let m such that
A4: n<=m;
m in NAT by ORDINAL1:def 12;
then |.(s*').m - g*'.| = |.(s.m)*' - g*'.| by Def2
.= |.(s.m - g)*'.| by COMPLEX1:34
.= |.s.m - g.| by COMPLEX1:53;
hence |.(s*').m - (lim s)*'.| < p by A3,A4;
end;
s1*' is convergent;
hence thesis by A2,Def6;
end;
begin :: Main Theorems
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 + s2 -> convergent for Complex_Sequence;
coherence
proof let s be Complex_Sequence such that
A1: s = s1 + s2;
consider g such that
A2: for p be Real st 0<p ex n st for m st n<=m holds |.s1.m-g.|<p
by Def5;
consider g9 such that
A3: for p be Real st 0<p ex n st for m st n<=m holds |.s2.m-g9.|<p
by Def5;
take g1 = g + g9;
let p be Real;
assume
A4: p>0;
then consider n1 such that
A5: for m st n1<=m holds |.s1.m - g.|<p/2 by A2;
consider n2 such that
A6: for m st n2<=m holds |.s2.m - g9.|<p/2 by A3,A4;
reconsider n = max(n1,n2) as Element of NAT by ORDINAL1:def 12;
take n;
let m such that
A7: n<=m;
n2<=n by XXREAL_0:25;
then n + n2 <= n + m by A7,XREAL_1:7;
then n2<=m by XREAL_1:6;
then
A8: |.s2.m - g9.|<p/2 by A6;
m in NAT by ORDINAL1:def 12;
then
A9: |.(s1 + s2).m - g1.| = |.s1.m + s2.m - (g + g9).| by VALUED_1:1
.= |.(s1.m - g) + (s2.m - g9).|;
n1<=n by XXREAL_0:25;
then n + n1 <= n + m by A7,XREAL_1:7;
then n1<=m by XREAL_1:6;
then |.s1.m - g.|<p/2 by A5;
then |.s1.m - g.| + |.s2.m - g9.| < p/2 + p/2 by A8,XREAL_1:8;
then |.s1.m - g.| + |.s2.m - g9.| + |.(s1 + s2).m - g1.|
< p + (|.s1.m - g.| + |.s2.m - g9.|) by A9,COMPLEX1:56,XREAL_1:8;
hence thesis by A1,XREAL_1:6;
end;
end;
::$CT
theorem Th12:
for s,s9 being convergent Complex_Sequence
holds lim (s + s9)=(lim s)+ (lim s9)
proof
let s,s9 be convergent Complex_Sequence;
for p be Real st 0<p ex n st for m st n<=m
holds |.(s + s9).m-((lim s)+(
lim s9)).|<p
proof
let p be Real;
assume 0<p;
then
A1: 0<p/2;
then consider n1 such that
A2: for m st n1<=m holds |.s.m-lim s.|<p/2 by Def6;
consider n2 such that
A3: for m st n2<=m holds |.s9.m-lim s9.|<p/2 by A1,Def6;
reconsider n = max(n1,n2) as Element of NAT by ORDINAL1:def 12;
take n;
let m such that
A4: n<=m;
n2<=n by XXREAL_0:25;
then n + n2 <= n + m by A4,XREAL_1:7;
then n2<=m by XREAL_1:6;
then
A5: |.s9.m-lim s9.|<p/2 by A3;
m in NAT by ORDINAL1:def 12;
then
A6: |.(s + s9).m-((lim s)+(lim s9)).| = |.s.m + s9.m - ((lim s)+(lim s9))
.| by VALUED_1:1
.=|.(s.m -lim s) + (s9.m - lim s9).|;
n1<=n by XXREAL_0:25;
then n + n1 <= n + m by A4,XREAL_1:7;
then n1<=m by XREAL_1:6;
then |.s.m-lim s.|<p/2 by A2;
then |.s.m-lim s.| + |.s9.m-lim s9.| < p/2 + p/2 by A5,XREAL_1:8;
then |.s.m-lim s.| + |.s9.m -lim s9.| + |.(s + s9).m-((lim s)+(lim s9)).|
< p + (|.s.m-lim s.| + |.s9.m -lim s9.|) by A6,COMPLEX1:56,XREAL_1:8;
hence thesis by XREAL_1:6;
end;
hence thesis by Def6;
end;
::$CT
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s + s9)*' = (lim s)*' + (lim s9)*'
proof
let s,s9 be convergent Complex_Sequence;
thus lim (s + s9)*' = (lim (s + s9))*' by Th11
.= ((lim s) + (lim s9))*' by Th12
.= (lim s)*' + (lim s9)*' by COMPLEX1:32;
end;
registration
let s be convergent Complex_Sequence, c be Complex;
cluster c(#)s -> convergent for Complex_Sequence;
coherence
proof
A1: now
let c be Element of COMPLEX;
per cases;
suppose
A2: c =0c;
now
let n;
thus (c(#)s).n = 0c*s.n by A2,VALUED_1:6
.= 0c;
end;
hence c(#)s is convergent by Th9;
end;
suppose
A3: c <> 0c;
thus c(#)s is convergent
proof
consider g such that
A4: for p be Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<
p by Def5;
take g9= c*g;
let p be Real such that
A5: 0<p;
A6: |.c.|>0 by A3,COMPLEX1:47;
consider n such that
A7: for m st n<=m holds |.s.m-g.|<p/|.c.| by A6,A4,A5;
take n;
let m;
assume n<=m;
then |.s.m-g.|<p/|.c.| by A7;
then |.s.m-g.|*|.c.|<p / |.c.|*|.c.| by A6,XREAL_1:68;
then |.s.m-g.|*|.c.|<p * (|.c.|)"*|.c.| by XCMPLX_0:def 9;
then |.s.m-g.|*|.c.|<p * ((|.c.|)"*|.c.|);
then
A8: |.s.m-g.|*|.c.|<p * 1 by A6,XCMPLX_0:def 7;
|.(c(#)s).m-g9.| = |.c*s.m-c*g.| by VALUED_1:6
.= |.c*(s.m-g).|
.= |.s.m-g.|*|.c.| by COMPLEX1:65;
hence thesis by A8;
end;
end;
end;
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
end;
::$CT
theorem Th14:
for s being convergent Complex_Sequence, r being Complex
holds lim(r(#)s)=r*(lim s)
proof
let s being convergent Complex_Sequence, r be Complex;
reconsider r as Element of COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A1: r<>0c;
for p be Real st p>0 holds ex n st for m st n<=m holds |.(r(#)s)
.m-r*(lim s).| <p
proof
let p be Real such that
A2: p>0;
A3: |.r.|>0 by A1,COMPLEX1:47;
p / |.r.| > 0 by A3,A2;
then consider n such that
A4: for m st n<=m holds |.s.m-(lim s).|< p/|.r.| by Def6;
take n;
let m;
assume n<=m;
then |.s.m-(lim s).|<p/|.r.| by A4;
then |.s.m-(lim s).|*|.r.|<p / |.r.|*|.r.| by A3,XREAL_1:68;
then |.s.m-(lim s).|*|.r.|< p * (|.r.|)"*|.r.| by XCMPLX_0:def 9;
then |.s.m-(lim s).|*|.r.|< p * ((|.r.|)"*|.r.|);
then
A5: |.s.m-(lim s).|*|.r.|< p * 1 by A3,XCMPLX_0:def 7;
|.(r(#)s).m - r*(lim s).|=|.r*s.m - r*(lim s).| by VALUED_1:6
.= |. r *(s.m-(lim s)).|
.= |.s.m-(lim s).|*|.r.| by COMPLEX1:65;
hence thesis by A5;
end;
hence thesis by Def6;
end;
suppose
A6: r=0c;
now
let n;
thus (r(#)s).n = 0c*s.n by A6,VALUED_1:6
.= 0c;
end;
hence thesis by A6,Th10;
end;
end;
::$CT
theorem
for s being convergent Complex_Sequence
holds lim (r(#)s)*' = (r*')*(lim s)*'
proof
let s being convergent Complex_Sequence;
thus lim (r(#)s)*' = (lim (r(#)s))*' by Th11
.= (r*(lim s))*' by Th14
.= (r*')*(lim s)*' by COMPLEX1:35;
end;
registration
let s be convergent Complex_Sequence;
cluster -s -> convergent for Complex_Sequence;
coherence;
end;
::$CT
theorem Th16:
for s being convergent Complex_Sequence
holds lim(-s)=-(lim s)
proof
let s being convergent Complex_Sequence;
lim(-s) = (-1)*(lim s) by Th14
.= - 1r*(lim s) by COMPLEX1:def 4;
hence thesis by COMPLEX1:def 4;
end;
::$CT
theorem
for s being convergent Complex_Sequence
holds lim (-s)*' = -(lim s)*'
proof
let s being convergent Complex_Sequence;
thus lim (-s)*' = (lim (-s))*' by Th11
.= (-(lim s))*' by Th16
.= -(lim s)*' by COMPLEX1:33;
end;
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 - s2 -> convergent for Complex_Sequence;
coherence
proof
- s2 is convergent;
hence thesis;
end;
end;
::$CT
theorem Th18:
for s,s9 being convergent Complex_Sequence
holds lim(s - s9)=(lim s)-( lim s9)
proof
let s,s9 be convergent Complex_Sequence;
lim(s - s9) = (lim s) + lim(-s9) by Th12
.= (lim s) + -(lim s9) by Th16;
hence thesis;
end;
::$CT
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s - s9)*' = (lim s)*' - (lim s9)*'
proof
let s,s9 be convergent Complex_Sequence;
thus lim (s - s9)*' = (lim (s - s9))*' by Th11
.= ((lim s) - (lim s9))*' by Th18
.= (lim s)*' - (lim s9)*' by COMPLEX1:34;
end;
registration
cluster convergent -> bounded for Complex_Sequence;
coherence
proof
let s;
assume s is convergent;
then consider g such that
A1: for p be Real st 0<p ex n st for m st n<=m holds |.s.m-g.|<p;
1 in NAT;
then reconsider j =1 as Element of REAL by NUMBERS:19;
consider n1 such that
A2: for m st n1<=m holds |.s.m-g.|<j by A1;
now
take R=|.g.| +1;
0+0 < R by COMPLEX1:46,XREAL_1:8;
hence 0<R;
let m;
A3: |.s.m.|- |.g.|+|.g.|=|.s.m.|;
assume n1<=m;
then
A4: |.s.m-g.|<1 by A2;
|.s.m.| - |.g.| <= |.s.m-g.| by COMPLEX1:59;
then |.s.m.| - |.g.| < 1 by A4,XXREAL_0:2;
hence |.s.m.|<R by A3,XREAL_1:6;
end;
then consider R1 be Real such that
A5: 0<R1 and
A6: for m st n1<=m holds |.s.m.|< R1;
consider R2 such that
A7: 0<R2 and
A8: for m st m<=n1 holds |.s.m.|< R2 by Th2;
reconsider R=R1+R2 as Real;
take R;
let m;
A9: R2+0 < R by A5,XREAL_1:8;
A10: now
assume m<=n1;
then |.s.m.|< R2 by A8;
hence thesis by A9,XXREAL_0:2;
end;
A11: R1+0 < R by A7,XREAL_1:8;
now
assume n1<=m;
then |.s.m.|< R1 by A6;
hence thesis by A11,XXREAL_0:2;
end;
hence thesis by A10;
end;
end;
registration
cluster non bounded -> non convergent for Complex_Sequence;
coherence;
end;
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 (#) s2 -> convergent for Complex_Sequence;
coherence
proof let s be Complex_Sequence such that
A1: s = s1 (#) s2;
consider g1 such that
A2: for p being Real st 0<p ex n st for m st n<=m holds |.s1.m-g1.|<p
by Def5;
consider g2 such that
A3: for p being Real st 0<p ex n st for m st n<=m holds |.s2.m-g2.|<p
by Def5;
take g=g1*g2;
let p be Real;
consider R such that
A4: 0<R and
A5: for n holds |.s1.n.|<R by Th8;
A6: 0+0<|.g2.|+R by A4,COMPLEX1:46,XREAL_1:8;
assume
A7: 0<p;
then consider n1 such that
A8: for m st n1<=m holds |.s1.m-g1.|<p/(|.g2.|+R) by A2,A6;
consider n2 such that
A9: for m st n2<=m holds |.s2.m-g2.|<p/(|.g2.|+R) by A3,A6,A7;
take n=n1+n2;
let m such that
A10: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A10,XXREAL_0:2;
then
A11: |.s1.m-g1.|<=p/(|.g2.|+R) by A8;
0<=|.g2.| & |.(s1.m-g1)*g2.|=|.g2.|*|.s1.m-g1.| by COMPLEX1:46,65;
then
A12: |.(s1.m-g1)*g2.|<=|.g2.|*(p/(|.g2.|+R)) by A11,XREAL_1:64;
|.((s1(#)s2).m)-g.|=|.(s1.m*s2.m) -s1.m*g2+s1.m*g2-g1*g2.| by VALUED_1:5
.=|.s1.m*(s2.m-g2)+(s1.m-g1)*g2.|;
then
A13: |.((s1(#)s2).m)-g.|<= |.s1.m*(s2.m-g2).|+|.(s1.m-g1)*g2.| by COMPLEX1:56;
n2<=n by NAT_1:12;
then n2<=m by A10,XXREAL_0:2;
then
A14: |.s2.m-g2.|<p/(|.g2.|+R) by A9;
A15: 0<=|.s1.m.| & 0<=|.s2.m-g2.| by COMPLEX1:46;
|.s1.m.|<R by A5;
then |.s1.m.|*|.s2.m-g2.|<R*(p/(|.g2.|+R)) by A15,A14,XREAL_1:96;
then
A16: |.s1.m*(s2.m-g2).|<R*(p/(|.g2.|+R)) by COMPLEX1:65;
R*(p/(|.g2.|+R))+|.g2.|*(p/(|.g2.|+R)) =(p/(|.g2.|+R))*(|.g2.|+R)
.=p by A6,XCMPLX_1:87;
then |.s1.m*(s2.m-g2).|+|.(s1.m-g1)*g2.|<p by A16,A12,XREAL_1:8;
hence thesis by A1,A13,XXREAL_0:2;
end;
end;
::$CT
theorem Th20:
for s,s9 being convergent Complex_Sequence
holds lim(s(#)s9)=(lim s)*(lim s9)
proof
let s,s9 be convergent Complex_Sequence;
consider R such that
A1: 0<R and
A2: for n holds |.s.n.|<R by Th8;
A3: 0+0<|.(lim s9).|+R by A1,COMPLEX1:46,XREAL_1:8;
A4: 0<=|.(lim s9).| by COMPLEX1:46;
now
let p be Real;
assume 0<p;
then
A5: 0<p/(|.(lim s9).|+R) by A3;
then consider n1 such that
A6: for m st n1<=m holds |.s.m-(lim s).|<p/(|.(lim s9).|+R) by Def6;
consider n2 such that
A7: for m st n2<=m holds |.s9.m-(lim s9).|<p/(|.(lim s9).|+R) by A5,Def6;
take n=n1+n2;
let m such that
A8: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A8,XXREAL_0:2;
then
A9: |.s.m-(lim s).|<=p/(|.(lim s9).|+R) by A6;
|.(s.m-(lim s))*(lim s9).| =|.(lim s9).|*|.s.m-(lim s).| by COMPLEX1:65;
then
A10: |.(s.m-(lim s))*(lim s9).|<=|.(lim s9).|* (p/(|.(lim s9).|+R)) by A4,A9,
XREAL_1:64;
A11: 0<=|.s.m.| & 0<=|.s9.m-(lim s9).| by COMPLEX1:46;
n2<=n by NAT_1:12;
then n2<=m by A8,XXREAL_0:2;
then
A12: |.s9.m-(lim s9).|<p/(|.(lim s9).|+R) by A7;
|.((s(#)s9).m)-(lim s)*(lim s9).| =|.(s.m*s9.m-s.m*(lim s9)+s.m*(lim
s9))- (lim s)*(lim s9).| by VALUED_1:5
.=|.s.m*(s9.m-(lim s9))+ (s.m-(lim s))*(lim s9).|;
then
A13: |.((s(#)s9).m)-(lim s)*(lim s9).|<= |.s.m*(s9.m-(lim s9)).|+|.(s.m-(
lim s))*(lim s9).| by COMPLEX1:56;
|.s.m.|<R by A2;
then |.s.m.|*|.s9.m-(lim s9).|<R*(p/(|.(lim s9).|+R)) by A11,A12,XREAL_1:96
;
then
A14: |.s.m*(s9.m-(lim s9)).|<R*(p/(|.(lim s9).|+R)) by COMPLEX1:65;
R*(p/(|.(lim s9).|+R))+|.(lim s9).|*(p/(|.(lim s9).|+R)) =(p/(|.(lim
s9).|+R))*(|.(lim s9).|+R)
.=p by A3,XCMPLX_1:87;
then |.s.m*(s9.m-(lim s9)).|+|.(s.m-(lim s))* (lim s9).|<p by A14,A10,
XREAL_1:8;
hence |.((s(#)s9).m)-(lim s)*(lim s9).|<p by A13,XXREAL_0:2;
end;
hence thesis by Def6;
end;
::$CT
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s(#)s9)*' = (lim s)*' * (lim s9)*'
proof
let s,s9 be convergent Complex_Sequence;
thus lim (s(#)s9)*' = (lim (s(#)s9))*' by Th11
.= ((lim s) * (lim s9))*' by Th20
.= (lim s)*' * (lim s9)*' by COMPLEX1:35;
end;
theorem Th22:
for s being convergent Complex_Sequence st lim s <> 0c
ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.|
proof
let s be convergent Complex_Sequence such that
A1: (lim s)<>0c;
0<|.(lim s).| by A1,COMPLEX1:47;
then 0<|.(lim s).|/2;
then consider n1 such that
A2: for m st n1<=m holds |.s.m-(lim s).|<|.(lim s).|/2 by Def6;
take n=n1;
let m;
assume n<=m;
then
A3: |.s.m-(lim s).|<|.(lim s).|/2 by A2;
A4: |.(lim s)-s.m.|=|.-(s.m-(lim s)).| .=|.s.m-(lim s).| by COMPLEX1:52;
A5: |.(lim s).|/2+(|.s.m.|- |.(lim s).|/2) =|.s.m.| & |.(lim s).|- |.s.m.|+
(|.s. m.|- |.(lim s).|/2) =|.(lim s).|/2;
|.(lim s).|- |.s.m.|<=|.(lim s)-s.m.| by COMPLEX1:59;
then |.(lim s).|- |.s.m.|<|.(lim s).|/2 by A3,A4,XXREAL_0:2;
hence thesis by A5,XREAL_1:6;
end;
theorem Th23:
for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero
holds s" is convergent
proof
let s be convergent Complex_Sequence;
assume that
A1: (lim s)<>0c and
A2: s is non-zero;
consider n1 such that
A3: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,Th22;
take(lim s)";
let p be Real;
assume
A4: 0<p;
A5: 0<|.(lim s).| by A1,COMPLEX1:47;
then 0*0<|.(lim s).|*|.(lim s).|;
then 0<(|.(lim s).|*|.(lim s).|)/2;
then 0*0<p*((|.(lim s).|*|.(lim s).|)/2) by A4;
then consider n2 such that
A6: for m st n2<=m holds |.s.m-(lim s).|<p*((|.(lim s).|*|.(lim s).|)/2
) by Def6;
take n=n1+n2;
let m such that
A7: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A7,XXREAL_0:2;
then
A8: |.(lim s).|/2<|.s.m.| by A3;
A9: 0<|.(lim s).|/2 by A5;
then 0*0<p*(|.(lim s).|/2) by A4;
then
A10: (p*(|.(lim s).|/2))/|.s.m.|< (p*(|.(lim s).|/2))/(|.(lim s).|/2) by A8,A9,
XREAL_1:76;
A11: 0<>|.(lim s).|/2 by A1,COMPLEX1:47;
A12: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s).|/
2 )" by XCMPLX_0:def 9
.=p*((|.(lim s).|/2)*(|.(lim s).|/2 )")
.=p*1 by A11,XCMPLX_0:def 7
.=p;
A13: 0<>|.(lim s).| by A1,COMPLEX1:47;
A14: (p*((|.(lim s).|*|.(lim s).|)/2))/(|.s.m.|*|.(lim s).|) =(p*(2"*(|.(lim
s).|*|.(lim s).|)))* (|.s.m.|*|.(lim s).|)" by XCMPLX_0:def 9
.=p*2"*((|.(lim s).|*|.(lim s).|)*(|.(lim s).|*|.s.m.|)")
.=p*2"*((|.(lim s).|*|.(lim s).|)* (|.(lim s).|"*|.s.m.|")) by XCMPLX_1:204
.=p*2"*(|.(lim s).|*(|.(lim s).|*|.(lim s).|")*|.s.m.|")
.=p*2"*(|.(lim s).|*1*|.s.m.|") by A13,XCMPLX_0:def 7
.=p*(|.(lim s).|/2)*|.s.m.|"
.=(p*(|.(lim s).|/2))/|.s.m.| by XCMPLX_0:def 9;
m in NAT by ORDINAL1:def 12;
then
A15: s.m <> 0 by A2,COMSEQ_1:3;
then s.m*(lim s)<>0c by A1;
then 0<|.s.m*(lim s).| by COMPLEX1:47;
then
A16: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65;
n2<=n by NAT_1:12;
then n2<=m by A7,XXREAL_0:2;
then |.s.m-(lim s).|<p*((|.(lim s).|*|.(lim s).|)/2) by A6;
then
A17: |.s.m-(lim s).|/(|.s.m.|*|.(lim s).|)< (p*((|.(lim s).|*|.(lim s).|)/2)
)/(|.s.m.|*|.(lim s).|) by A16,XREAL_1:74;
|.(s").m-(lim s)".|=|.(s.m)"-(lim s)".| by VALUED_1:10
.=|.s.m-(lim s).|/(|.s.m.|*|.(lim s).|) by A1,Th1,A15;
hence thesis by A17,A14,A10,A12,XXREAL_0:2;
end;
theorem Th24:
s is convergent & (lim s)<>0c & s is non-zero implies lim s"=( lim s)"
proof
assume that
A1: s is convergent and
A2: (lim s)<>0c and
A3: s is non-zero;
consider n1 such that
A4: for m st n1<=m holds |.(lim s).|/2<|.s.m.| by A1,A2,Th22;
A5: 0<|.(lim s).| by A2,COMPLEX1:47;
then 0*0<|.(lim s).|*|.(lim s).|;
then
A6: 0<(|.(lim s).|*|.(lim s).|)/2;
A7: 0<>|.(lim s).| by A2,COMPLEX1:47;
A8: now
let p be Real;
A9: 0<>|.(lim s).|/2 by A2,COMPLEX1:47;
A10: (p*(|.(lim s).|/2))/(|.(lim s).|/2 ) =(p*(|.(lim s).|/2))*(|.(lim s)
.|/2 )" by XCMPLX_0:def 9
.=p*((|.(lim s).|/2)*(|.(lim s).|/2 )")
.=p*1 by A9,XCMPLX_0:def 7
.=p;
assume
A11: 0<p;
then 0*0<p*((|.(lim s).|*|.(lim s).|)/2) by A6;
then consider n2 such that
A12: for m st n2<=m holds |.s.m-(lim s).|<p*((|.(lim s).|*|.(lim s).|)
/2) by A1,Def6;
take n=n1+n2;
let m such that
A13: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A13,XXREAL_0:2;
then
A14: |.(lim s).|/2<|.s.m.| by A4;
A15: 0<|.(lim s).|/2 by A5;
then 0*0<p*(|.(lim s).|/2) by A11;
then
A16: (p*(|.(lim s).|/2))/|.s.m.|< (p*(|.(lim s).|/2))/(|.(lim s).|/2) by A14
,A15,XREAL_1:76;
A17: (p*((|.(lim s).|*|.(lim s).|)/2))/(|.s.m.|*|.(lim s).|) =(p*(2"*(|.(
lim s).|*|.(lim s).|)))* (|.s.m.|*|.(lim s).|)" by XCMPLX_0:def 9
.=p*2"*((|.(lim s).|*|.(lim s).|)*(|.(lim s).|*|.s.m.|)")
.=p*2"*((|.(lim s).|*|.(lim s).|)* (|.(lim s).|"*|.s.m.|")) by
XCMPLX_1:204
.=p*2"*(|.(lim s).|*(|.(lim s).|*|.(lim s).|")*|.s.m.|")
.=p*2"*(|.(lim s).|*1*|.s.m.|") by A7,XCMPLX_0:def 7
.=p*(|.(lim s).|/2)*|.s.m.|"
.=(p*(|.(lim s).|/2))/|.s.m.| by XCMPLX_0:def 9;
m in NAT by ORDINAL1:def 12;
then
A18: s.m <> 0 by A3,COMSEQ_1:3;
then s.m*(lim s)<>0c by A2;
then 0<|.s.m*(lim s).| by COMPLEX1:47;
then
A19: 0<|.s.m.|*|.(lim s).| by COMPLEX1:65;
n2<=n by NAT_1:12;
then n2<=m by A13,XXREAL_0:2;
then |.s.m-(lim s).|<p*((|.(lim s).|*|.(lim s).|)/2) by A12;
then
A20: |.s.m-(lim s).|/(|.s.m.|*|.(lim s).|)< (p*((|.(lim s).|*|.(lim s).|)/
2))/(|.s.m.|*|.(lim s).|) by A19,XREAL_1:74;
|.(s").m-(lim s)".|=|.(s.m)"-(lim s)".| by VALUED_1:10
.=|.s.m-(lim s).|/(|.s.m.|*|.(lim s).|) by A2,Th1,A18;
hence |.(s").m-(lim s)".|<p by A20,A17,A16,A10,XXREAL_0:2;
end;
s" is convergent by A1,A2,A3,Th23;
hence thesis by A8,Def6;
end;
::$CT
theorem
s is convergent & (lim s)<>0c & s is non-zero implies lim (s")*' = ((
lim s)*')"
proof
assume
A1: s is convergent & (lim s)<>0c & s is non-zero;
then s" is convergent by Th23;
hence lim (s")*' = (lim s")*' by Th11
.= ((lim s)")*' by A1,Th24
.= ((lim s)*')" by COMPLEX1:36;
end;
theorem Th26:
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies s9/"s is convergent
proof
assume that
A1: s9 is convergent and
A2: s is convergent & (lim s)<>0c & s is non-zero;
s" is convergent by A2,Th23;
hence thesis by A1;
end;
theorem Th27:
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim(s9/"s)=(lim s9)/(lim s)
proof
assume that
A1: s9 is convergent and
A2: s is convergent & (lim s)<>0c & s is non-zero;
s" is convergent by A2,Th23;
then lim (s9(#)(s"))=(lim s9)*(lim s") by A1,Th20
.=(lim s9)*(lim s)" by A2,Th24
.=(lim s9)/(lim s) by XCMPLX_0:def 9;
hence thesis;
end;
::$CT
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*')
proof
assume
A1: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero;
then s9/"s is convergent by Th26;
hence lim (s9/"s)*' = (lim (s9/"s))*' by Th11
.= ((lim s9)/(lim s))*' by A1,Th27
.= ((lim s9)*')/((lim s)*') by COMPLEX1:37;
end;
theorem Th29:
s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent
proof
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: (lim s) = 0c;
take g=0c;
consider R such that
A4: 0<R and
A5: for m holds |.s1.m.|<R by A2,Th8;
let p be Real such that
A6: 0<p;
A7: 0<p/R by A6,A4;
then consider n1 such that
A8: for m st n1<=m holds |.s.m-0c.|<p/R by A1,A3,Def6;
take n=n1;
let m such that
A9: n<=m;
A10: |.((s(#)s1).m)-g.|=|.s.m*s1.m.| by VALUED_1:5
.=|.s.m.|*|.s1.m.| by COMPLEX1:65;
|.s.m.|=|.s.m-0c.|;
then
A11: |.s.m.|<p/R by A8,A9;
now
(p/R)*R=p*R"*R by XCMPLX_0:def 9
.=p*(R"*R)
.=p*1 by A4,XCMPLX_0:def 7
.=p;
then
A12: (p/R)*|.s1.m.|<p by A5,A7,XREAL_1:68;
A13: 0<=|.s1.m.| by COMPLEX1:46;
assume |.s1.m.|<>0;
then |.((s(#)s1).m)-g.|<(p/R)*|.s1.m.| by A11,A10,A13,XREAL_1:68;
hence thesis by A12,XXREAL_0:2;
end;
hence thesis by A6,A10;
end;
theorem Th30:
s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1) =0c
proof
assume that
A1: s is convergent and
A2: s1 is bounded and
A3: lim s=0c;
A4: now
consider R such that
A5: 0<R and
A6: for m holds |.s1.m.|<R by A2,Th8;
let p be Real such that
A7: 0<p;
A8: 0<p/R by A7,A5;
then consider n1 such that
A9: for m st n1<=m holds |.s.m-0c.|<p/R by A1,A3,Def6;
take n=n1;
let m;
(p/R)*R=p*R"*R by XCMPLX_0:def 9
.=p*(R"*R)
.=p*1 by A5,XCMPLX_0:def 7;
then
A10: (p/R)*|.s1.m.|<p by A6,A8,XREAL_1:68;
assume n<=m;
then
A11: |.s.m-0c.|<p/R by A9;
A12: |.((s(#)s1).m)-0c.|=|.s.m*s1.m.| by VALUED_1:5
.=|.s.m.|*|.s1.m.| by COMPLEX1:65;
A13: 0<=|.s1.m.| by COMPLEX1:46;
now
assume |.s1.m.|<>0;
then |.((s(#)s1).m)-0c.|<(p/R)*|.s1.m.| by A11,A12,A13,XREAL_1:68;
hence |.((s(#)s1).m)-0c.|<p by A10,XXREAL_0:2;
end;
hence |.((s(#)s1).m)-0c.|<p by A7,A12;
end;
s(#)s1 is convergent by A1,A2,A3,Th29;
hence thesis by A4,Def6;
end;
::$CT
theorem
s is convergent & s1 is bounded & (lim s)=0c implies lim (s(#)s1)*' = 0c
proof
assume
A1: s is convergent & s1 is bounded & (lim s)=0c;
then s(#)s1 is convergent by Th29;
hence lim (s(#)s1)*' = (lim (s(#)s1))*' by Th11
.= 0c by A1,Th30,COMPLEX1:28;
end;