The Mizar article:

The Limit of a Real Function at Infinity

by
Jaroslaw Kotowicz

Received August 20, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: LIMFUNC1
[ MML identifier index ]


environ

 vocabulary ARYTM, SEQ_1, PARTFUN1, ARYTM_1, RELAT_1, BOOLE, SQUARE_1, ARYTM_3,
      PROB_1, RCOMP_1, SEQ_2, FUNCT_1, ORDINAL2, ABSVALUE, SEQM_3, LATTICES,
      RFUNCT_1, RFUNCT_2, FINSEQ_1, LIMFUNC1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, PROB_1, RELSET_1,
      SQUARE_1, PARTFUN1, RFUNCT_1, RCOMP_1, RFUNCT_2;
 constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, SQUARE_1,
      RFUNCT_1, RCOMP_1, RFUNCT_2, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters RELSET_1, XREAL_0, SEQ_1, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, SEQ_2, XBOOLE_0;
 theorems AXIOMS, TARSKI, REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4,
      SQUARE_1, RFUNCT_1, RFUNCT_2, PROB_1, RCOMP_1, FUNCT_1, FUNCT_2, XREAL_0,
      XBOOLE_0, XBOOLE_1, REAL_2, FINSEQ_2, XCMPLX_0, XCMPLX_1;
 schemes SEQ_1, RCOMP_1;

begin

reserve r,r1,r2,g,g1,g2 for real number;
reserve n,m,k for Nat;
reserve seq,seq1,seq2 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

Lm1: (-1)*(-1)=1;
Lm2: 0<g & r<=r1 implies r-g<r1 & r<r1+g
proof assume A1: 0<g & r<=r1; then r-g<r1-0 by REAL_1:92;
 hence r-g<r1; r+0<r1+g by A1,REAL_1:67; hence thesis;
end;

Lm3: rng seq c=dom(f1+f2) implies dom(f1+f2)=dom f1/\dom f2 &
rng seq c=dom f1 & rng seq c=dom f2
proof assume A1: rng seq c=dom(f1+f2);
 thus dom(f1+f2)=dom f1/\dom f2 by SEQ_1:def 3; then dom(f1+f2)c=dom f1 &
 dom(f1+f2)c=dom f2 by XBOOLE_1:17;hence thesis by A1,XBOOLE_1:1;
end;

Lm4: rng seq c=dom(f1(#)f2) implies dom(f1(#)f2)=dom f1/\dom f2 &
rng seq c=dom f1 & rng seq c=dom f2
proof assume A1: rng seq c=dom(f1(#)f2);
 thus dom(f1(#)f2)=dom f1/\dom f2 by SEQ_1:def 5; then dom(f1(#)f2)c=dom f1 &
 dom(f1(#)f2)c=dom f2 by XBOOLE_1:17; hence thesis by A1,XBOOLE_1:1;
end;

definition let n,m;
  redefine func max(n,m) ->Nat;
  coherence by FINSEQ_2:1;
end;

theorem Th1:
0<=r1 & r1<r2 & 0<g1 & g1<=g2 implies r1*g1<r2*g2
proof assume A1: 0<=r1 & r1<r2 & 0<g1 & g1<=g2; then A2: r1*g1<=r1*g2 by AXIOMS
:25;
   0<g2 by A1; then r1*g2<r2*g2 by A1,REAL_1:70;
 hence thesis by A2,AXIOMS:22;
end;

definition let r be real number;
  redefine func halfline(r);
  synonym left_open_halfline(r);
end;

reserve r,r1,r2,g,g1,g2 for Real;

definition let r be real number;
func left_closed_halfline(r) ->Subset of REAL equals :Def1: {g: g<=r};
coherence
 proof now let x be set; assume x in {g: g<=r}; then ex g st x=g & g<=r;
hence x in REAL;
  end; hence thesis by TARSKI:def 3;
 end;
func right_closed_halfline(r) ->Subset of REAL equals :Def2: {g: r<=g};
coherence
 proof now let x be set; assume x in {g: r<=g}; then ex g st x=g & r<=g;
hence x in REAL;
  end; hence thesis by TARSKI:def 3;
 end;
func right_open_halfline(r) ->Subset of REAL equals :Def3: {g: r<g};
coherence
 proof now let x be set; assume x in {g: r<g}; then ex g st x=g & r<g;
hence x in REAL;
  end; hence thesis by TARSKI:def 3;
 end;
end;

canceled 6;

theorem
  r1<=r2 implies right_open_halfline(r2) c= right_open_halfline(r1)
proof assume A1: r1<=r2; let x be set;
assume x in right_open_halfline(r2);
 then x in {r: r2<r} by Def3; then consider r such that
 A2: r=x & r2<r; r1<r by A1,A2,AXIOMS:22; then x in {g: r1<g} by A2;
 hence thesis by Def3;
end;

theorem
  r1<=r2 implies right_closed_halfline(r2) c= right_closed_halfline(r1)
proof assume A1: r1<=r2; let x be set;
 assume x in right_closed_halfline(r2);
 then x in {r: r2<=r} by Def2; then consider r such that
 A2: r=x & r2<=r; r1<=r by A1,A2,AXIOMS:22; then x in {g: r1<=g} by A2;
 hence thesis by Def2;
end;

theorem
  right_open_halfline(r) c= right_closed_halfline(r)
proof let x be set; assume x in right_open_halfline(r);
 then x in {r2: r<r2} by Def3;
 then consider r1 such that A1: r1=x & r<r1;
   x in {g: r<=g} by A1; hence thesis by Def2;
end;

theorem
  ].r,g.[ c= right_open_halfline(r)
proof let x be set; assume x in ].r,g.[;
 then x in {r1: r<r1 & r1<g} by RCOMP_1:def 2;
 then ex g1 st g1=x & r<g1 & g1<g;
 then x in {g2: r<g2}; hence thesis by Def3;
end;

theorem
  [.r,g.] c= right_closed_halfline(r)
proof let x be set; assume x in [.r,g.];
 then x in {r1: r<=r1 & r1<=g} by RCOMP_1:def 1;
 then ex g1 st g1=x & r<=g1 & g1<=g;
 then x in {g2: r<=g2}; hence thesis by Def2;
end;

theorem
  r1<=r2 implies left_open_halfline(r1) c= left_open_halfline(r2)
proof assume A1: r1<=r2; let x be set; assume x in left_open_halfline(r1);
 then x in {r: r<r1} by PROB_1:def 15; then consider r such that A2: r=x & r<
r1;
   r<r2 by A1,A2,AXIOMS:22; then x in {g: g<r2} by A2
; hence thesis by PROB_1:def 15;
end;

theorem
  r1<=r2 implies left_closed_halfline(r1) c= left_closed_halfline(r2)
proof assume A1: r1<=r2;
 let x be set; assume x in left_closed_halfline(r1);
 then x in {r: r<=r1} by Def1
;
 then consider r such that A2: r=x & r<=r1; r<=r2 by A1,A2,AXIOMS:22;
 then x in {g: g<=r2} by A2; hence thesis by Def1;
end;

theorem
  left_open_halfline(r) c= left_closed_halfline(r)
proof let x be set; assume x in left_open_halfline(r);
 then x in {r2: r2<r} by PROB_1:def 15; then consider r1 such that A1: r1=x &
r1<r;
   x in {g: g<=r} by A1; hence thesis by Def1;
end;

theorem
  ].g,r.[ c= left_open_halfline(r)
proof let x be set; assume x in ].g,r.[;
then x in {r1: g<r1 & r1<r} by RCOMP_1:def 2
;
 then ex g1 st g1=x & g<g1 & g1<r;
 then x in {g2: g2<r}; hence thesis by PROB_1:def 15;
end;

theorem
  [.g,r.] c= left_closed_halfline(r)
proof let x be set; assume x in [.g,r.];
then x in {r1: g<=r1 & r1<=r} by RCOMP_1:def 1;
 then ex g1 st g1=x & g<=g1 & g1<=r;
 then x in {g2: g2<=r}; hence thesis by Def1;
end;

theorem Th18:
left_open_halfline(r) /\ right_open_halfline(g) = ].g,r.[
proof thus left_open_halfline(r)/\right_open_halfline(g)c=].g,r.[
 proof let x be set; assume x in left_open_halfline(r)/\right_open_halfline(g)
;
  then A1: x in left_open_halfline(r) &
  x in right_open_halfline(g) by XBOOLE_0:def 3
;
  then x in {r1: r1<r} by PROB_1:def 15; then A2: ex t1 be Real st
 t1=x & t1<r; x in {g1: g<g1} by A1,Def3; then ex g1 st g1=x & g<g1;
then x in {g2: g<g2 & g2<r} by A2; hence x in ].g,r.[ by RCOMP_1:def 2;
 end;
 let x be set; assume x in ].g,r.[;
 then x in {r1: g<r1 & r1<r} by RCOMP_1:def 2
;
 then A3: ex r2 st r2=x & g<r2 & r2<r; then x in {g1: g<g1};
 then A4: x in right_open_halfline(g) by Def3; x in {g2: g2<r} by A3;
 then x in left_open_halfline(r) by PROB_1:def 15; hence thesis by A4,XBOOLE_0:
def 3
;
end;

theorem Th19:
left_closed_halfline(r) /\ right_closed_halfline(g) = [.g,r.]
proof thus left_closed_halfline(r)/\right_closed_halfline(g)c=[.g,r.]
 proof let x be set;
 assume x in left_closed_halfline(r)/\right_closed_halfline(g);
  then A1: x in left_closed_halfline(r) & x in right_closed_halfline(g) by
XBOOLE_0:def 3
;
  then x in {r1: r1<=r} by Def1; then A2: ex t1 be Real st
 t1=x & t1<=r; x in {g1: g<=g1} by A1,Def2; then ex g1 st g1=x & g<=g1;
then x in {g2: g<=g2 & g2<=r} by A2; hence x in [.g,r.] by RCOMP_1:def 1;
 end;
 let x be set; assume x in [.g,r.];
 then x in {r1: g<=r1 & r1<=r} by RCOMP_1:def 1
;
 then A3: ex r2 st r2=x & g<=r2 & r2<=r;
 then x in {g1: g<=g1}; then A4: x in right_closed_halfline(g) by Def2;
   x in {g2: g2<=r} by A3; then x in left_closed_halfline(r) by Def1;
 hence thesis by A4,XBOOLE_0:def 3;
end;

theorem
  r<=r1 implies ].r1,r2.[ c= right_open_halfline(r) &
[.r1,r2.] c= right_closed_halfline(r)
proof assume A1: r<=r1; thus ].r1,r2.[c=right_open_halfline(r)
 proof let x be set; assume x in ].r1,r2.[;
 then x in {g: r1<g & g<r2} by RCOMP_1:def 2;
  then consider g1 such that A2: x=g1 & r1<g1 & g1<r2; r<g1 by A1,A2,AXIOMS:22
;
  then x in {g2: r<g2} by A2; hence thesis by Def3;
 end;
 let x be set;
 assume x in [.r1,r2.]; then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1
;
 then consider g1 such that A3: x=g1 & r1<=g1 & g1<=r2; r<=
g1 by A1,A3,AXIOMS:22;
 then x in {g2: r<=g2} by A3; hence thesis by Def2;
end;

theorem
  r<r1 implies [.r1,r2.] c= right_open_halfline(r)
proof assume A1: r<r1; let x be set; assume x in [.r1,r2.];
 then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1; then consider g1 such that
 A2: x=g1 & r1<=g1 & g1<=r2; r<g1 by A1,A2,AXIOMS:22;
 then x in {g2: r<g2} by A2; hence thesis by Def3;
end;

theorem
  r2<=r implies ].r1,r2.[ c= left_open_halfline(r) &
[.r1,r2.] c= left_closed_halfline(r)
proof assume A1: r2<=r; thus ].r1,r2.[c=left_open_halfline(r)
 proof let x be set; assume x in ].r1,r2.[;
 then x in {g: r1<g & g<r2} by RCOMP_1:def 2;
  then consider g1 such that A2: x=g1 & r1<g1 & g1<r2; g1<r by A1,A2,AXIOMS:22
;
  then x in {g2: g2<r} by A2; hence thesis by PROB_1:def 15;
 end;
 let x be set; assume x in [.r1,r2.];
 then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1
;
 then consider g1 such that A3: x=g1 & r1<=g1 & g1<=r2; g1<=
r by A1,A3,AXIOMS:22;
 then x in {g2: g2<=r} by A3; hence thesis by Def1;
end;

theorem
  r2<r implies [.r1,r2.] c= left_open_halfline(r)
proof assume A1: r2<r; let x be set; assume x in [.r1,r2.];
 then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1; then consider g1 such that
 A2: x=g1 & r1<=g1 & g1<=r2; g1<r by A1,A2,AXIOMS:22;
 then x in {g2: g2<r} by A2; hence thesis by PROB_1:def 15;
end;

theorem Th24:
REAL \ right_open_halfline(r) = left_closed_halfline(r) &
REAL \ right_closed_halfline(r) = left_open_halfline(r) &
REAL \ left_open_halfline(r) = right_closed_halfline(r) &
REAL \ left_closed_halfline(r) = right_open_halfline(r)
proof now let x be set;
 thus x in REAL\right_open_halfline(r) implies x in left_closed_halfline(r)
 proof assume A1: x in REAL\right_open_halfline(r);
  then A2: x in REAL & not x in right_open_halfline(r) by XBOOLE_0:def 4;
  reconsider x'=x as Real by A1,XBOOLE_0:def 4;
    not x' in {g: r<g} by A2,Def3;
  then x'<=r; then x in {g1: g1<=r}; hence thesis by Def1;
 end;
 thus x in left_closed_halfline(r) implies x in REAL\right_open_halfline(r)
 proof assume x in left_closed_halfline(r);
  then x in {r2: r2<=r} by Def1; then A3: ex g2 st x=g2 & g2<=r;
 then not ex g2 st x=g2 & r<g2;
  then not x in {g1: r<g1}; then not x in right_open_halfline(r) by Def3;
  hence thesis by A3,XBOOLE_0:def 4;
 end;
 end; hence REAL\right_open_halfline(r)=left_closed_halfline(r) by TARSKI:2;
   now let x be set;
 thus x in REAL\right_closed_halfline(r) implies x in left_open_halfline(r)
 proof assume A4: x in REAL\right_closed_halfline(r);
  then A5: x in REAL & not x in right_closed_halfline(r) by XBOOLE_0:def 4;
  reconsider x'=x as Real by A4,XBOOLE_0:def 4; not x' in {g: r<=g} by A5,Def2
;
then x'<r; then x in {g1: g1<r};
  hence thesis by PROB_1:def 15;
 end;
 thus x in left_open_halfline(r) implies x in REAL\right_closed_halfline(r)
 proof assume x in left_open_halfline(r);
  then x in {r2: r2<r} by PROB_1:def 15; then A6: ex g2 st x=g2 & g2<r;
 then not ex g1 st x=g1 & r<=g1;
  then not x in {g: r<=g}; then not x in right_closed_halfline(r) by Def2;
  hence thesis by A6,XBOOLE_0:def 4;
 end;
end; hence REAL\right_closed_halfline(r)=left_open_halfline(r) by TARSKI:2;
   now let x be set;
 thus x in REAL\left_open_halfline(r) implies x in right_closed_halfline(r)
 proof assume A7: x in REAL\left_open_halfline(r);
  then A8: x in REAL & not x in left_open_halfline(r) by XBOOLE_0:def 4;
  reconsider x'=x as Real by A7,XBOOLE_0:def 4;
    not x' in {g: g<r} by A8,PROB_1:def 15;
  then r<=x'; then x in {g1: r<=g1}; hence thesis by Def2;
 end;
 thus x in right_closed_halfline(r) implies x in REAL\left_open_halfline(r)
 proof assume x in right_closed_halfline(r);
  then x in {r2: r<=r2} by Def2; then A9: ex g2 st x=g2 & r<=g2;
 then not ex g2 st x=g2 & g2<r;
  then not x in {g1: g1<r}; then not x in left_open_halfline(r) by PROB_1:def
15;
  hence thesis by A9,XBOOLE_0:def 4;
 end;
 end; hence REAL\left_open_halfline(r)=right_closed_halfline(r) by TARSKI:2;
   now let x be set;
 thus x in REAL\left_closed_halfline(r) implies x in right_open_halfline(r)
 proof assume A10: x in REAL\left_closed_halfline(r);
  then A11: x in REAL & not x in left_closed_halfline(r) by XBOOLE_0:def 4;
  reconsider x'=x as Real by A10,XBOOLE_0:def 4
; not x' in {g: g<=r} by A11,Def1;
then r<x'; then x in {g1: r<g1};
  hence thesis by Def3;
 end;
 thus x in right_open_halfline(r) implies x in REAL\left_closed_halfline(r)
 proof assume x in right_open_halfline(r);
  then x in {r2: r<r2} by Def3; then A12: ex g2 st x=g2 & r<g2;
 then not ex g1 st x=g1 & g1<=r;
  then not x in {g: g<=r}; then not x in left_closed_halfline(r) by Def1;
  hence thesis by A12,XBOOLE_0:def 4;
 end;
end; hence thesis by TARSKI:2;
end;

theorem
  REAL \ ].r1,r2.[ = left_closed_halfline(r1) \/ right_closed_halfline(r2) &
REAL \ [.r1,r2.] = left_open_halfline(r1) \/ right_open_halfline(r2)
proof
 thus REAL\].r1,r2.[=REAL\(left_open_halfline(r2)/\right_open_halfline(r1))
  by Th18
 .=(REAL\left_open_halfline(r2))\/(REAL\right_open_halfline(r1)) by XBOOLE_1:54
 .=right_closed_halfline(r2)\/ (REAL\right_open_halfline(r1)) by Th24
 .=left_closed_halfline(r1)\/ right_closed_halfline(r2) by Th24;
 thus REAL\[.r1,r2.]=REAL\(left_closed_halfline(r2)/\right_closed_halfline(r1)
)
  by Th19
 .=(REAL\left_closed_halfline(r2))\/
(REAL\right_closed_halfline(r1)) by XBOOLE_1:54
 .=right_open_halfline(r2)\/ (REAL\right_closed_halfline(r1)) by Th24
 .=left_open_halfline(r1)\/ right_open_halfline(r2) by Th24;
end;

theorem Th26:
(seq is non-decreasing implies seq is bounded_below) &
(seq is non-increasing implies seq is bounded_above)
proof
thus seq is non-decreasing implies seq is bounded_below
 proof assume A1: seq is non-decreasing; take seq.0-1;
  let n; A2: seq.0-1<seq.0-0 by REAL_1:92;
    seq.0<=seq.n by A1,SEQM_3:21; hence thesis by A2,AXIOMS:22;
 end;
 assume A3: seq is non-increasing; take seq.0+1;
 let n; A4: seq.0+0<seq.0+1 by REAL_1:67; seq.n<=seq.0 by A3,SEQM_3:22;
 hence thesis by A4,AXIOMS:22;
end;

theorem Th27:
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies
for n holds seq.n<0
proof assume that
 A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing and
 A2: ex n st not seq.n<0; consider n such that A3: not seq.n<0 by A2;
   now per cases by A3;
 suppose A4: 0<seq.n; then consider n1 be Nat such that
  A5: for m st n1<=m holds abs(seq.m-0)<seq.n by A1,SEQ_2:def 7;
    n1<=n1+n by NAT_1:37; then A6: abs(seq.(n1+n)-0)<seq.n by A5;
  A7: n<=n1+n by NAT_1:37; then 0<seq.(n1+n) by A1,A4,SEQM_3:12;
  then seq.(n1+n)<seq.n by A6,ABSVALUE:def 1;
  hence contradiction by A1,A7,SEQM_3:12;
 suppose seq.n=0; hence contradiction by A1,SEQ_1:7;
 end; hence contradiction;
end;

theorem Th28:
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies
for n holds 0<seq.n
proof assume that
 A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing and
 A2: ex n st not 0<seq.n; consider n such that A3: not 0<seq.n by A2;
   now per cases by A3;
 suppose A4: seq.n<0; then 0<-seq.n by REAL_1:26,50;
  then consider n1 be Nat such that
  A5: for m st n1<=m holds abs(seq.m-0)<-seq.n by A1,SEQ_2:def 7;
    n1<=n1+n by NAT_1:37; then A6: abs(seq.(n1+n)-0)<-seq.n by A5;
  A7: n<=n1+n by NAT_1:37; then seq.(n1+n)<0 by A1,A4,SEQM_3:14;
  then -seq.(n1+n)<-seq.n by A6,ABSVALUE:def 1; then seq.n<seq.(n1+n) by REAL_1
:50;
  hence contradiction by A1,A7,SEQM_3:14;
 suppose seq.n=0; hence contradiction by A1,SEQ_1:7;
 end; hence contradiction;
end;

theorem Th29:
seq is convergent & 0<lim seq implies ex n st for m st n<=m holds 0<seq.m
proof assume that A1: seq is convergent & 0<lim seq and
 A2: for n ex m st n<=m & not 0<seq.m; consider n such that
 A3: for m st n<=m holds abs(seq.m-lim seq)<lim seq by A1,SEQ_2:def 7;
 consider m such that A4: n<=m & not 0<seq.m by A2;
 A5: abs(seq.m-lim seq)<lim seq by A3,A4;
   now per cases by A4;
 suppose A6: seq.m<0; then seq.m-lim seq<0-0 by A1,REAL_1:92;
then -(seq.m-lim seq)<lim seq by A5,ABSVALUE:def 1;
  then lim seq-seq.m<lim seq by XCMPLX_1:143;
  then lim seq<lim seq+seq.m by REAL_1:84;
  then lim seq - lim seq<seq.m by REAL_1:84;
hence contradiction by A6,XCMPLX_1:14;
 suppose seq.m=0; then abs(-lim seq)<lim seq by A5,XCMPLX_1:150;
  then abs(lim seq)<lim seq by ABSVALUE:17;
  hence contradiction by A1,ABSVALUE:def 1;
 end; hence contradiction;
end;

theorem Th30:
seq is convergent & 0<lim seq implies
ex n st for m st n<=m holds (lim seq)/2<seq.m
proof assume A1: seq is convergent & 0<lim seq;
 deffunc U(set) = (lim seq)/2;
 consider s1 be Real_Sequence such that
 A2: for n holds s1.n= U(n) from ExRealSeq;
 A3: s1 is constant by A2,SEQM_3:def 6; s1.0=(lim seq)/2 by A2;
 then lim(seq-s1)=lim seq-(lim seq)/2 by A1,A3,SEQ_4:59
 .=(lim seq)/2+(lim seq)/2-(lim seq)/2 by XCMPLX_1:66
 .=(lim seq)/2 by XCMPLX_1:26;
 then A4: 0<lim(seq-s1) by A1,SEQ_2:3;
   s1 is convergent by A3,SEQ_4:39; then seq-s1 is convergent by A1,SEQ_2:25
;
 then consider n such that A5: for m st n<=m holds 0<(seq-s1).m by A4,Th29;
 take n; let m; assume n<=m; then 0<(seq-s1).m by A5;
 then 0<seq.m-s1.m by RFUNCT_2:6; then 0<seq.m-(lim seq)/2 by A2;
 then 0+(lim seq)/2<seq.m by REAL_1:86; hence thesis;
end;

definition let seq;
 attr seq is divergent_to+infty means :Def4:
  for r ex n st for m st n<=m holds r<seq.m;
 attr seq is divergent_to-infty means :Def5:
  for r ex n st for m st n<=m holds seq.m<r;
end;

canceled 2;

theorem
  seq is divergent_to+infty or seq is divergent_to-infty implies
ex n st for m st n<=m holds seq^\m is_not_0
proof assume A1: seq is divergent_to+infty or seq is divergent_to-infty;
   now per cases by A1;
 suppose seq is divergent_to+infty; then consider n such that
  A2: for m st n<=m holds 0<seq.m by Def4; take n; let m such that A3: n<=m;
    now let k; n<=k+m by A3,NAT_1:37;
   then 0<seq.(k+m) by A2; hence 0<>(seq^\m).k by SEQM_3:def 9;
  end; hence seq^\m is_not_0 by SEQ_1:7;
 suppose seq is divergent_to-infty; then consider n such that
  A4: for m st n<=m holds seq.m<0 by Def5; take n; let m such that A5: n<=m;
    now let k; n<=k+m by A5,NAT_1:37;
   then seq.(k+m)<0 by A4; hence (seq^\m).k<>0 by SEQM_3:def 9;
  end; hence seq^\m is_not_0 by SEQ_1:7;
 end; hence thesis;
end;

theorem Th34:
(seq^\k is divergent_to+infty implies seq is divergent_to+infty) &
(seq^\k is divergent_to-infty implies seq is divergent_to-infty)
proof
thus seq^\k is divergent_to+infty implies seq is divergent_to+infty
 proof assume A1: seq^\k is divergent_to+infty; let r;
  consider n1 be Nat such that
  A2: for m st n1<=m holds r<(seq^\k).m by A1,Def4;
  take n=n1+k; let m; assume n<=m; then consider n2 be Nat such that
  A3: m=n+n2 by NAT_1:28;
  A4: n1+n2+k=m by A3,XCMPLX_1:1; n1<=n1+n2 by NAT_1:37
; then r<(seq^\k).(n1+n2) by A2;
  hence r<seq.m by A4,SEQM_3:def 9;
 end;
 assume A5: seq^\k is divergent_to-infty; let r; consider n1 be Nat such that
 A6: for m st n1<=m holds (seq^\k).m<r by A5,Def5;
 take n=n1+k; let m; assume n<=m; then consider n2 be Nat such that
 A7: m=n+n2 by NAT_1:28;
 A8: n1+n2+k=m by A7,XCMPLX_1:1; n1<=n1+n2 by NAT_1:37; then (seq^\k).(n1+n2
)<
r
by A6;
 hence seq.m<r by A8,SEQM_3:def 9;
end;

theorem Th35:
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1+seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to+infty & seq2 is divergent_to+infty; let r
;
 consider n1 be Nat such that A2: for m st n1<=m holds r/2<seq1.m by A1,Def4;
 consider n2 be Nat such that A3: for m st n2<=m holds r/2<seq2.m by A1,Def4;
 take n=max(n1,n2); let m such that A4: n<=m;
   n1<=n by SQUARE_1:46; then n1<=m by A4,AXIOMS:22; then A5: r/2<seq1.m by A2
;
   n2<=n by SQUARE_1:46; then n2<=m by A4,AXIOMS:22; then r/2<seq2.m by A3;
 then r/2+r/2<seq1.m+seq2.m by A5,REAL_1:67; then r<seq1.m+seq2.m by XCMPLX_1:
66;
 hence thesis by SEQ_1:11;
end;

theorem Th36:
seq1 is divergent_to+infty & seq2 is bounded_below implies
seq1+seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to+infty & seq2 is bounded_below;
 then consider M be real number such that
 A2: for n holds M<seq2.n by SEQ_2:def 4;
 let r;
   r-M is Real by XREAL_0:def 1;
 then consider n such that A3: for m st n<=m holds r-M<seq1.m by A1,Def4;
 take n; let m; assume n<=m; then A4: r-M<seq1.m by A3;
   M<seq2.m by A2; then r-M+M<seq1.m+seq2.m by A4,REAL_1:67;
 then r<seq1.m+seq2.m by XCMPLX_1:27; hence thesis by SEQ_1:11;
end;

theorem Th37:
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1(#)seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to+infty & seq2 is divergent_to+infty; let r
;
 consider n1 be Nat such that A2: for m st n1<=m holds sqrt abs(r)<seq1.m
  by A1,Def4;
 consider n2 be Nat such that A3: for m st n2<=m holds sqrt abs(r)<seq2.m
  by A1,Def4; take n=max(n1,n2); let m such that A4: n<=m;
   n1<=n by SQUARE_1:46; then n1<=
m by A4,AXIOMS:22; then A5: sqrt abs(r)<seq1.m by A2;
   n2<=n by SQUARE_1:46; then n2<=
m by A4,AXIOMS:22; then A6: sqrt abs(r)<seq2.m by A3;
 A7: abs(r)>=0 by ABSVALUE:5; then sqrt abs(r)>=0 by SQUARE_1:def 4;
 then (sqrt abs(r))*(sqrt abs(r))<seq1.m*seq2.m by A5,A6,SEQ_2:7;
 then (sqrt abs(r))^2<seq1.m*seq2.m by SQUARE_1:def 3;
 then A8: abs(r)<seq1.m*seq2.m by A7,SQUARE_1:def 4;
   r<=abs(r) by ABSVALUE:11; then r<seq1.m*seq2.m by A8,AXIOMS:22;
 hence thesis by SEQ_1:12;
end;

theorem Th38:
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1+seq2 is divergent_to-infty
proof assume A1: seq1 is divergent_to-infty & seq2 is divergent_to-infty; let r
;
 consider n1 be Nat such that A2: for m st n1<=m holds seq1.m<r/2 by A1,Def5;
 consider n2 be Nat such that A3: for m st n2<=m holds seq2.m<r/2 by A1,Def5;
 take n=max(n1,n2); let m such that A4: n<=m;
   n1<=n by SQUARE_1:46; then n1<=m by A4,AXIOMS:22; then A5: seq1.m<r/2 by A2
;
   n2<=n by SQUARE_1:46; then n2<=m by A4,AXIOMS:22; then seq2.m<r/2 by A3;
 then seq1.m+seq2.m<r/2+r/2 by A5,REAL_1:67; then seq1.m+seq2.m<r by XCMPLX_1:
66;
 hence thesis by SEQ_1:11;
end;

theorem Th39:
seq1 is divergent_to-infty & seq2 is bounded_above implies
seq1+seq2 is divergent_to-infty
proof assume A1: seq1 is divergent_to-infty & seq2 is bounded_above;
 then consider M be real number such that
 A2: for n holds seq2.n<M by SEQ_2:def 3;
 let r;
   r-M is Real by XREAL_0:def 1;
 then consider n such that A3: for m st n<=m holds seq1.m<r-M by A1,Def5;
 take n; let m; assume n<=m; then A4: seq1.m<r-M by A3;
   seq2.m<M by A2; then seq1.m+seq2.m<r-M+M by A4,REAL_1:67;
 then seq1.m+seq2.m<r by XCMPLX_1:27; hence thesis by SEQ_1:11;
end;

theorem Th40:
(seq is divergent_to+infty & r>0 implies r(#)seq is divergent_to+infty) &
(seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty) &
(seq is divergent_to+infty & r=0 implies rng (r(#)seq)={0} & r(#)
seq is constant)
proof
thus seq is divergent_to+infty & r>0 implies r(#)seq is divergent_to+infty
 proof assume A1: seq is divergent_to+infty & r>0; let g;
  consider n such that A2: for m st n<=m holds g/r<seq.m by A1,Def4;
 take n; let m; assume n<=m; then g/r<seq.m by A2;
  then g/r*r<r*seq.m by A1,REAL_1:70; then g<r*seq.m by A1,XCMPLX_1:88;
  hence thesis by SEQ_1:13;
 end;
thus seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty
 proof assume A3: seq is divergent_to+infty & r<0; let g;
  consider n such that A4: for m st n<=m holds g/r<seq.m by A3,Def4;
 take n; let m; assume n<=m; then g/r<seq.m by A4;
  then r*seq.m<g/r*r by A3,REAL_1:71; then r*seq.m<g by A3,XCMPLX_1:88;
  hence thesis by SEQ_1:13;
 end;
 assume A5: seq is divergent_to+infty & r=0;
 thus rng(r(#)seq)={0}
 proof
 thus rng(r(#)seq)c={0}
  proof let x be set; assume x in rng(r(#)seq); then consider n such that
  A6: x=(r(#)seq).n by RFUNCT_2:9;
     x=r*seq.n by A6,SEQ_1:13
   .=0 by A5; hence x in {0} by TARSKI:def 1;
  end;
  let x be set; assume x in {0}; then A7: x=0 by TARSKI:def 1;
     now thus (r(#)seq).0=r*seq.0 by SEQ_1:13
    .=0 by A5;
   end; hence x in rng(r(#)seq) by A7,RFUNCT_2:9;
 end; hence thesis by SEQM_3:15;
end;

theorem Th41:
(seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty) &
(seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty) &
(seq is divergent_to-infty & r=0 implies rng (r(#)seq)={0} & r(#)
seq is constant)
proof
thus seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty
 proof assume A1: seq is divergent_to-infty & r>0; let g;
  consider n such that A2: for m st n<=m holds seq.m<g/r by A1,Def5;
 take n; let m; assume n<=m; then seq.m<g/r by A2;
  then r*seq.m<g/r*r by A1,REAL_1:70; then r*seq.m<g by A1,XCMPLX_1:88;
  hence thesis by SEQ_1:13;
 end;
thus seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty
 proof assume A3: seq is divergent_to-infty & r<0; let g;
  consider n such that A4: for m st n<=m holds seq.m<g/r by A3,Def5;
 take n; let m; assume n<=m; then seq.m<g/r by A4;
  then g/r*r<r*seq.m by A3,REAL_1:71; then g<r*seq.m by A3,XCMPLX_1:88;
  hence thesis by SEQ_1:13;
 end;
 assume A5: seq is divergent_to-infty & r=0;
 thus rng(r(#)seq)={0}
 proof
 thus rng(r(#)seq)c={0}
  proof let x be set; assume x in rng(r(#)seq);
   then consider n such that A6: x=(r(#)seq).n by RFUNCT_2:9;
     x=r*seq.n by A6,SEQ_1:13
   .=0 by A5; hence x in {0} by TARSKI:def 1;
  end;
  let x be set; assume x in {0}; then A7: x=0 by TARSKI:def 1;
     now thus (r(#)seq).0=r*seq.0 by SEQ_1:13
    .=0 by A5;
   end; hence x in rng(r(#)seq) by A7,RFUNCT_2:9;
 end; hence thesis by SEQM_3:15;
end;

theorem
  (seq is divergent_to+infty implies -seq is divergent_to-infty) &
(seq is divergent_to-infty implies -seq is divergent_to+infty)
proof A1: (-1)(#)seq=-seq by SEQ_1:25;
 hence seq is divergent_to+infty implies -seq is divergent_to-infty by Th40;
 assume seq is divergent_to-infty; hence thesis by A1,Th41;
end;

theorem
  seq is bounded_below & seq1 is divergent_to-infty implies
seq-seq1 is divergent_to+infty
proof assume A1: seq is bounded_below & seq1 is divergent_to-infty;
 A2: (-1)(#)seq1+seq=seq+-seq1 by SEQ_1:25
 .=seq-seq1 by SEQ_1:15;
   (-1)(#)seq1 is divergent_to+infty by A1,Th41; hence thesis by A1,A2,Th36;
end;

theorem
  seq is bounded_above & seq1 is divergent_to+infty implies
seq-seq1 is divergent_to-infty
proof assume A1: seq is bounded_above & seq1 is divergent_to+infty;
 A2: (-1)(#)seq1+seq=seq+-seq1 by SEQ_1:25
 .=seq-seq1 by SEQ_1:15;
   (-1)(#)seq1 is divergent_to-infty by A1,Th40; hence thesis by A1,A2,Th39;
end;

theorem
  seq is divergent_to+infty & seq1 is convergent implies
 seq+seq1 is divergent_to+infty
proof assume A1: seq is divergent_to+infty & seq1 is convergent;
 then seq1 is bounded by SEQ_2:27; then seq1 is bounded_below by SEQ_2:def 5;
 hence thesis by A1,Th36;
end;

theorem
  seq is divergent_to-infty & seq1 is convergent implies
 seq+seq1 is divergent_to-infty
proof assume A1: seq is divergent_to-infty & seq1 is convergent;
 then seq1 is bounded by SEQ_2:27; then seq1 is bounded_above by SEQ_2:def 5;
 hence thesis by A1,Th39;
end;

theorem Th47:
(for n holds seq.n=n) implies seq is divergent_to+infty
proof assume A1: for n holds seq.n=n; let r;
 consider n such that A2: r<n by SEQ_4:10; take n; let m; assume n<=m;
 then r<m by A2,AXIOMS:22; hence r<seq.m by A1;
end;

theorem Th48:
(for n holds seq.n=-n) implies seq is divergent_to-infty
proof assume A1: for n holds seq.n=-n;
 deffunc U(Nat) = $1;
consider s1 be Real_Sequence such that
 A2: for n holds s1.n=U(n) from ExRealSeq;
 s1 is divergent_to+infty by A2,Th47;
 then (-1)(#)s1 is divergent_to-infty by Th40;
 then A3: -s1 is divergent_to-infty by SEQ_1:25;
   now let n; thus (-s1).n=-s1.n by SEQ_1:14
  .=-n by A2
  .=seq.n by A1;
 end; hence thesis by A3,FUNCT_2:113;
end;

theorem Th49:
seq1 is divergent_to+infty & (ex r st r>0 & for n holds seq2.n>=r) implies
seq1(#)seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to+infty & ex r st r>0 &
 for n holds seq2.n>=r;
 then consider M be Real such that A2: M>0 & for n holds seq2.n>=M;
 let r; consider n such that
 A3: for m st n<=m holds abs(r)/M<seq1.m by A1,Def4;
 take n; let m; assume n<=m; then A4: abs(r)/M<seq1.m by A3;
 A5: M<=seq2.m by A2; 0<=abs(r) by ABSVALUE:5;
 then abs(r)/M>=0 by A2,SQUARE_1:27;
 then abs(r)/M*M<seq1.m*seq2.m by A2,A4,A5,Th1;
then A6: abs(r)<seq1.m*seq2.m by A2,XCMPLX_1:88; r<=abs(r) by ABSVALUE:11;
 then r<seq1.m*seq2.m by A6,AXIOMS:22; hence thesis by SEQ_1:12;
end;

theorem
  seq1 is divergent_to-infty & (ex r st 0<r & for n holds seq2.n>=r) implies
seq1(#)seq2 is divergent_to-infty
proof assume A1: seq1 is divergent_to-infty &
 (ex r st 0<r & for n holds seq2.n>=r);
 then (-1)(#)seq1 is divergent_to+infty by Th41;
then A2: (-1)(#)seq1(#)seq2 is divergent_to+infty by A1,Th49;
   (-1)(#)((-1)(#)seq1(#)seq2)=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:26
 .=1(#)(seq1(#)seq2) by Lm1,SEQ_1:31
 .=seq1(#)seq2 by SEQ_1:35; hence thesis by A2,Th40;
end;

theorem Th51:
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1(#)seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to-infty & seq2 is divergent_to-infty;
 then A2: (-1)(#)seq1 is divergent_to+infty by Th41;
A3: (-1)(#)seq2 is divergent_to+infty by A1,Th41;
   (-1)(#)seq1(#)((-1)(#)seq2)=(-1)(#)(seq1(#)((-1)(#)seq2)) by SEQ_1:26
 .=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:27
 .=1(#)(seq1(#)seq2) by Lm1,SEQ_1:31
 .=seq1(#)seq2 by SEQ_1:35; hence thesis by A2,A3,Th37;
end;

theorem Th52:
(seq is divergent_to+infty or seq is divergent_to-infty) implies
abs(seq) is divergent_to+infty
proof assume A1: seq is divergent_to+infty or seq is divergent_to-infty; let r;
   now per cases by A1;
 suppose seq is divergent_to+infty;
  then consider n such that A2: for m st n<=m holds abs(r)<seq.m by Def4;
  take n; let m; seq.m<=abs(seq.m) by ABSVALUE:11;
  then A3: seq.m<=abs(seq).m by SEQ_1:16; A4: r<=abs(r) by ABSVALUE:11;
  assume n<=m; then abs(r)<seq.m by A2; then r<seq.m by A4,AXIOMS:22;
  hence r<abs(seq).m by A3,AXIOMS:22;
 suppose seq is divergent_to-infty;
  then consider n such that A5: for m st n<=m holds seq.m<-r by Def5;
  take n; let m; -abs(seq.m)<=seq.m by ABSVALUE:11;
  then A6: -abs(seq).m<=seq.m by SEQ_1:16; assume n<=m; then seq.m<-r by A5;
  then -abs(seq).m<-r by A6,AXIOMS:22; hence r<abs(seq).m by REAL_1:50;
 end; hence thesis;
end;

theorem Th53:
seq is divergent_to+infty & seq1 is_subsequence_of seq implies
seq1 is divergent_to+infty
proof assume A1: seq is divergent_to+infty & seq1 is_subsequence_of seq;
 then consider Ns be increasing Seq_of_Nat such that A2: seq1=seq*Ns by SEQM_3:
def 10
;
 let r; consider n such that A3: for m st n<=m holds r<seq.m by A1,Def4;
 take n; let m; A4: m<=Ns.m by SEQM_3:33; assume n<=m;
 then n<=Ns.m by A4,AXIOMS:22; then r<seq.(Ns.m) by A3;
 hence r<seq1.m by A2,SEQM_3:31;
end;

theorem Th54:
seq is divergent_to-infty & seq1 is_subsequence_of seq implies
seq1 is divergent_to-infty
proof assume A1: seq is divergent_to-infty & seq1 is_subsequence_of seq;
 then consider Ns be increasing Seq_of_Nat such that A2: seq1=seq*Ns by SEQM_3:
def 10
;
 let r; consider n such that A3: for m st n<=m holds seq.m<r by A1,Def5;
 take n; let m; A4: m<=Ns.m by SEQM_3:33;
 assume n<=m; then n<=Ns.m by A4,AXIOMS:22; then seq.(Ns.m)<r by A3;
 hence seq1.m<r by A2,SEQM_3:31;
end;

theorem
  seq1 is divergent_to+infty & seq2 is convergent & 0<lim seq2 implies
seq1(#)seq2 is divergent_to+infty
proof assume A1: seq1 is divergent_to+infty &
 seq2 is convergent & 0<lim seq2;
 then consider n1 be Nat such that
 A2: for m st n1<=m holds (lim seq2)/2<seq2.m by Th30;
   seq1^\n1 is_subsequence_of seq1 by SEQM_3:47;
 then A3: seq1^\n1 is divergent_to+infty by A1,Th53;
   now thus 0<(lim seq2)/2 by A1,SEQ_2:3;
  let n; n1<=n+n1 by NAT_1:37;
  then (lim seq2)/2<seq2.(n+n1) by A2;
  hence (lim seq2)/2<=(seq2^\n1).n by SEQM_3:def 9;
 end; then (seq1^\n1)(#)(seq2^\n1) is divergent_to+infty by A3,Th49;
 then (seq1(#)seq2)^\n1 is divergent_to+infty by SEQM_3:42; hence thesis by
Th34;
end;

theorem Th56:
seq is non-decreasing & not seq is bounded_above implies
 seq is divergent_to+infty
proof assume A1: seq is non-decreasing & not seq is bounded_above;
 let r; consider n such that A2: r+1<=seq.n by A1,SEQ_2:def 3; take n; let m;
 assume n<=m; then seq.n<=seq.m by A1,SEQM_3:12;
  then r+1<=seq.m by A2,AXIOMS:22;
 hence thesis by Lm2;
end;

theorem Th57:
seq is non-increasing & not seq is bounded_below implies
 seq is divergent_to-infty
proof assume A1: seq is non-increasing & not seq is bounded_below;
 let r; consider n such that A2: seq.n<=r-1 by A1,SEQ_2:def 4;
 take n; let m; assume n<=m; then seq.m<=seq.n by A1,SEQM_3:14;
  then seq.m<=r-1 by A2,AXIOMS:22;
 hence thesis by Lm2;
end;

theorem
  seq is increasing & not seq is bounded_above implies seq is
divergent_to+infty
proof assume A1: seq is increasing & not seq is bounded_above;
 then seq is non-decreasing by SEQM_3:23; hence thesis by A1,Th56;
end;

theorem
  seq is decreasing & not seq is bounded_below implies seq is
divergent_to-infty
proof assume A1: seq is decreasing & not seq is bounded_below;
 then seq is non-increasing by SEQM_3:24; hence thesis by A1,Th57;
end;

theorem
  seq is monotone implies seq is convergent or seq is divergent_to+infty or
seq is divergent_to-infty
proof assume A1: seq is monotone;
   now per cases by A1,SEQM_3:def 7;
 suppose A2: seq is non-decreasing; then A3: seq is bounded_below by Th26;
    now per cases;
  suppose seq is bounded_above; then A4: seq is bounded by A3,SEQ_2:def 5;
     seq is monotone by A2,SEQM_3:def 7;
   hence thesis by A4,SEQ_4:53;
  suppose not seq is bounded_above;
   hence thesis by A2,Th56;
  end; hence thesis;
 suppose A5: seq is non-increasing; then A6: seq is bounded_above by Th26;
    now per cases;
  suppose seq is bounded_below; then A7: seq is bounded by A6,SEQ_2:def 5;
     seq is monotone by A5,SEQM_3:def 7;
   hence thesis by A7,SEQ_4:53;
  suppose not seq is bounded_below;
   hence thesis by A5,Th57;
  end; hence thesis;
 end; hence thesis;
end;

theorem Th61:
(seq is divergent_to+infty or seq is divergent_to-infty) implies
seq" is convergent & lim(seq")=0
proof assume that A1: seq is divergent_to+infty or
 seq is divergent_to-infty;
   now per cases by A1;
 suppose A2: seq is divergent_to+infty;
  A3: now let r be real number such that A4: 0<r;
     r" is Real by XREAL_0:def 1;
   then consider n such that A5: for m st n<=m holds r"<seq.m by A2,Def4;
   take n; let m; A6: 0<r" by A4,REAL_1:72;
   assume n<=m; then A7: r"<seq.m by A5; then A8: 0<seq.m by A6,AXIOMS:22;
   1/seq.m<1/r" by A6,A7,SEQ_2:10;
then A9: 1/seq.m<r by XCMPLX_1:218;
   A10: 1/seq.m=(seq.m)" by XCMPLX_1:217; A11: 0<(seq.m)" by A8,REAL_1:72;
      (seq.m)"=(seq").m by SEQ_1:def 8;
hence abs((seq").m-0)<r by A9,A10,A11,ABSVALUE:def 1;
  end; hence seq" is convergent by SEQ_2:def 6;
  hence thesis by A3,SEQ_2:def 7;
 suppose A12: seq is divergent_to-infty;
  A13: now let r be real number such that A14: 0<r;
    -(r") is Real by XREAL_0:def 1;
   then consider n such that A15: for m st n<=m holds seq.m<-(r") by A12,Def5;
   take n; let m; A16: 0<r" by A14,REAL_1:72;
   then A17: -(r")<0 by REAL_1:26,50;
 assume n<=m; then A18: seq.m<-(r") by A15;
   then A19: seq.m<0 by A16,REAL_1:26,50;
   A20: (-1)"=-1;
     1/(-(r"))<1/seq.m by A17,A18,REAL_2:200; then (-(1*(r")))"<1/seq.m by
XCMPLX_1:217;
then ((-1)*(r"))"<1/seq.m by XCMPLX_1:175;
   then A21: (-1)*(r"")<1/seq.m by A20,XCMPLX_1:205;
     1/seq.m<0/seq.m by A19,REAL_1:74;
then abs(1/seq.m)=-(1/seq.m) by ABSVALUE:def 1;
   then -(1*r)<-abs(1/seq.m) by A21,XCMPLX_1:175; then abs(1/seq.m)<r by REAL_1
:50;
   then abs((seq.m)")<r by XCMPLX_1:217; hence abs((seq").m-0)<r by SEQ_1:def 8
;
  end; hence seq" is convergent by SEQ_2:def 6; hence thesis by A13,SEQ_2:def 7
;
 end; hence thesis;
end;

theorem Th62:
seq is_not_0 & seq is convergent & lim seq=0 &
(ex k st for n st k<=n holds 0<seq.n) implies
seq" is divergent_to+infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0;
 given k such that A2: for n st k<=n holds 0<seq.n; let r; set l=abs(r)+1;
   0<=abs(r) by ABSVALUE:5; then 0<l by Lm2;
  then 0<l" by REAL_1:72; then consider o be Nat such that
 A3: for n st o<=n holds abs(seq.n-0)<l" by A1,SEQ_2:def 7;
   r<=abs(r) by ABSVALUE:11;
 then A4: r<l by Lm2; take m=max(k,o); let n;
 assume A5: m<=n; o<=m by SQUARE_1:46; then o<=n by A5,AXIOMS:22;
 then A6: abs(seq.n-0)<l" by A3; k<=m by SQUARE_1:46;
 then k<=n by A5,AXIOMS:22; then A7: 0<seq.n by A2;
 then seq.n<l" by A6,ABSVALUE:def 1; then 1/(l")<1/seq.n by A7,SEQ_2:10;
then l<1/seq.n by XCMPLX_1:218;
 then r<1/seq.n by A4,AXIOMS:22; then r<(seq.n)" by XCMPLX_1:217;
 hence r<(seq").n by SEQ_1:def 8;
end;

theorem Th63:
seq is_not_0 & seq is convergent & lim seq=0 &
(ex k st for n st k<=n holds seq.n<0) implies
seq" is divergent_to-infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0;
 given k such that A2: for n st k<=n holds seq.n<0; let r; set l=abs(r)+1;
   0<=abs(r) by ABSVALUE:5; then 0<l by Lm2;
  then 0<l" by REAL_1:72; then consider o be Nat such that
 A3: for n st o<=n holds abs(seq.n-0)<l" by A1,SEQ_2:def 7;
   -abs(r)<=r by ABSVALUE:11;
 then A4: -abs(r)-1<r by Lm2;
 A5: -l=-(1*l)
 .=(-1)*l by XCMPLX_1:175
 .=(-1)*abs(r)+(-1)*1 by XCMPLX_1:8
 .=-(1*abs(r))+(-1)*1 by XCMPLX_1:175
 .=-abs(r)-1 by XCMPLX_0:def 8; take m=max(k,o); let n;
 assume A6: m<=n; o<=m by SQUARE_1:46;
 then o<=n by A6,AXIOMS:22; then A7: abs(seq.n-0)<l" by A3; k<=m by SQUARE_1:46
; then k<= n by A6,AXIOMS:22;
 then A8: seq.n<0 by A2; then A9: 0<-(seq.n) by REAL_1:66;
   -(seq.n)<l" by A7,A8,ABSVALUE:def 1;
 then 1/(l")<1/(-(seq.n)) by A9,SEQ_2:10;
then l<1/(-(seq.n)) by XCMPLX_1:218;
 then l<(-(seq.n))" by XCMPLX_1:217; then l<-((seq.n)") by XCMPLX_1:224;
 then --((seq.n)")<-l by REAL_1:50;
 then (seq.n)"<r by A4,A5,AXIOMS:22; hence (seq").n<r by SEQ_1:def 8;
end;

theorem Th64:
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies
seq" is divergent_to-infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 &
 seq is non-decreasing;
 then for n holds 0<=n implies seq.n<0 by Th27; hence thesis by A1,Th63;
end;

theorem Th65:
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies
seq" is divergent_to+infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 &
 seq is non-increasing;
 then for n holds 0<=n implies 0<seq.n by Th28; hence thesis by A1,Th62;
end;

theorem
  seq is_not_0 & seq is convergent & lim seq=0 & seq is increasing implies
seq" is divergent_to-infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 &
 seq is increasing; then seq is non-decreasing by SEQM_3:23;
 hence thesis by A1,Th64;
end;

theorem
  seq is_not_0 & seq is convergent & lim seq=0 & seq is decreasing implies
seq" is divergent_to+infty
proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 &
 seq is decreasing; then seq is non-increasing by SEQM_3:24;
 hence thesis by A1,Th65;
end;

theorem
  seq1 is bounded & (seq2 is divergent_to+infty or seq2 is divergent_to-infty)
&
seq2 is_not_0 implies seq1/"seq2 is convergent & lim(seq1/"seq2)=0
proof assume A1: seq1 is bounded &
 (seq2 is divergent_to+infty or seq2 is divergent_to-infty) & seq2 is_not_0;
 then A2: seq2" is convergent & lim(seq2")=0 by Th61;
   (seq2")(#)
seq1=seq1/"seq2 by SEQ_1:def 9; hence thesis by A1,A2,SEQ_2:39,40;
end;

theorem Th69:
seq is divergent_to+infty & (for n holds seq.n<=seq1.n) implies
seq1 is divergent_to+infty
proof assume A1: seq is divergent_to+infty & (for n holds seq.n<=
seq1.n); let r;
 consider n such that A2: for m st n<=m holds r<seq.m by A1,Def4;
 take n; let m; A3: seq.m<=seq1.m by A1; assume n<=m;
 then r<seq.m by A2; hence r<seq1.m by A3,AXIOMS:22;
end;

theorem Th70:
seq is divergent_to-infty & (for n holds seq1.n<=seq.n) implies
seq1 is divergent_to-infty
proof assume A1: seq is divergent_to-infty & (for n holds seq1.n<=
seq.n); let r;
 consider n such that A2: for m st n<=m holds seq.m<r by A1,Def5;
 take n; let m; A3: seq1.m<=seq.m by A1; assume n<=m; then seq.m<r by A2;
 hence seq1.m<r by A3,AXIOMS:22;
end;

definition let f;
attr f is convergent_in+infty means :Def6:
 (for r ex g st r<g & g in dom f) &
 ex g st for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is convergent & lim(f*seq)=g;
attr f is divergent_in+infty_to+infty means :Def7:
 (for r ex g st r<g & g in dom f) &
 for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is divergent_to+infty;
attr f is divergent_in+infty_to-infty means :Def8:
 (for r ex g st r<g & g in dom f) &
 for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is divergent_to-infty;
attr f is convergent_in-infty means :Def9:
 (for r ex g st g<r & g in dom f) &
 ex g st for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is convergent & lim(f*seq)=g;
attr f is divergent_in-infty_to+infty means :Def10:
 (for r ex g st g<r & g in dom f) &
 for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is divergent_to+infty;
attr f is divergent_in-infty_to-infty means :Def11:
 (for r ex g st g<r & g in dom f) &
 for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is divergent_to-infty;
end;

canceled 6;

theorem
  f is convergent_in+infty iff
(for r ex g st r<g & g in dom f) &
(ex g st for g1 st 0<g1 ex r st for r1 st r<r1 &
 r1 in dom f holds abs(f.r1-g)<g1)
proof thus f is convergent_in+infty implies
(for r ex g st r<g & g in dom f) &
(ex g st for g1 st 0<g1 ex r st for r1 st
 r<r1 & r1 in dom f holds abs(f.r1-g)<g1)
 proof assume A1: f is convergent_in+infty; then consider g2 such that
  A2: for seq st seq is divergent_to+infty & rng seq c=dom f holds
  f*seq is convergent & lim(f*seq)=g2 by Def6;
  assume not (for r ex g st r<g & g in dom f) or
  for g ex g1 st 0<g1 & for r
  ex r1 st r<r1 & r1 in dom f & abs(f.r1-g)>=g1;
  then consider g such that
  A3: 0<g & for r ex r1 st r<r1 & r1 in dom f & abs(f.r1-g2)>=g by A1,Def6;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f & abs(f.$2-g2)>=g;
  A4: now let n; consider r such that A5: n<r & r in dom f &
  abs(f.r-g2)>=g by A3;
   reconsider r as real number;
   take r; thus X[n,r] by A5;
  end; consider s be Real_Sequence such that
A6: for n holds X[n,s.n] from RealSeqChoice(A4);
 deffunc U(Nat) = $1;
  consider s1 be Real_Sequence such that
  A7: for n holds s1.n=U(n) from ExRealSeq;
  A8: s1 is divergent_to+infty by A7,Th47;
    now let n; n<s.n by A6; hence s1.n<=s.n by A7;end;
  then A9: s is divergent_to+infty by A8,Th69;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A6;
  end; then A10: rng s c=dom f by TARSKI:def 3;
  then f*s is convergent & lim(f*s)=g2 by A2,A9; then consider n such that
  A11: for m st n<=m holds abs((f*s).m-g2)<g by A3,SEQ_2:def 7;
    abs((f*s).n-g2)<g by A11; then abs(f.(s.n)-g2)<g by A10,RFUNCT_2:21;
  hence contradiction by A6;
 end;
 assume A12: for r ex g st r<g & g in dom f; given g such that
 A13: for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1;
   now let s be Real_Sequence such that
  A14: s is divergent_to+infty & rng s c=dom f;
  A15: now let g1 be real number;
A16:  g1 is Real by XREAL_0:def 1;
  assume 0<g1; then consider r such that
   A17: for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1 by A13,A16;
   consider n such that A18: for m st n<=m holds r<s.m by A14,Def4;
   take n; let m; assume n<=m; then A19: r<s.m by A18;
     s.m in rng s by RFUNCT_2:10;
   then abs(f.(s.m)-g)<g1 by A14,A17,A19; hence abs((f*s).m-g)<g1
     by A14,RFUNCT_2:21;
  end; hence f*s is convergent by SEQ_2:def 6;
  hence lim(f*s)=g by A15,SEQ_2:def 7;
 end; hence thesis by A12,Def6;
end;

theorem
  f is convergent_in-infty iff
(for r ex g st g<r & g in dom f) &
ex g st for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds
  abs(f.r1-g)<g1
proof thus f is convergent_in-infty implies
(for r ex g st g<r & g in dom f) &
(ex g st for g1 st 0<g1
 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1)
 proof assume A1: f is convergent_in-infty; then consider g2 such that
  A2: for seq st seq is divergent_to-infty & rng seq c=dom f holds
  f*seq is convergent & lim(f*seq)=g2 by Def9;
  assume not (for r ex g st g<r & g in dom f) or
  for g ex g1 st 0<g1 & for r
  ex r1 st r1<r & r1 in dom f & abs(f.r1-g)>=g1;
  then consider g such that
  A3: 0<g & for r ex r1 st r1<r & r1 in dom f & abs(f.r1-g2)>=g by A1,Def9;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f & abs(f.$2-g2)>=g;
  A4: now let n; consider r such that
  A5: r<-n & r in dom f & abs(f.r-g2)>=g by A3;
   reconsider r as real number;
   take r; thus X[n,r] by A5;
  end; consider s be Real_Sequence such that
  A6: for n holds X[n,s.n] from RealSeqChoice(A4);
 deffunc U(Nat) = -$1;
  consider s1 be Real_Sequence such that
  A7: for n holds s1.n=U(n) from ExRealSeq;
  A8: s1 is divergent_to-infty by A7,Th48;
    now let n; s.n<-n by A6; hence s.n<=s1.n by A7;end;
  then A9: s is divergent_to-infty by A8,Th70;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A6;
  end; then A10: rng s c=dom f by TARSKI:def 3;
  then f*s is convergent & lim(f*s)=g2 by A2,A9;
  then consider n such that A11: for m st n<=m holds abs((f*s).m-g2)<g by A3,
SEQ_2:def 7;
    abs((f*s).n-g2)<g by A11; then abs(f.(s.n)-g2)<g by A10,RFUNCT_2:21;
  hence contradiction by A6;
 end;
 assume A12: for r ex g st g<r & g in dom f; given g such that
 A13: for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1;
   now let s be Real_Sequence such that
  A14: s is divergent_to-infty & rng s c=dom f;
  A15: now let g1 be real number;
A16:  g1 is Real by XREAL_0:def 1;
  assume 0<g1; then consider r such that
   A17: for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 by A13,A16;
   consider n such that A18: for m st n<=m holds s.m<r by A14,Def5;
   take n; let m; assume n<=m; then A19: s.m<r by A18;
     s.m in rng s by RFUNCT_2:10;
   then abs(f.(s.m)-g)<g1 by A14,A17,A19;
   hence abs((f*s).m-g)<g1 by A14,RFUNCT_2:21;
  end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A15,SEQ_2:
def 7;
 end; hence thesis by A12,Def9;
end;

theorem
  f is divergent_in+infty_to+infty iff
 (for r ex g st r<g & g in dom f) &
 for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1
proof thus f is divergent_in+infty_to+infty implies
(for r ex g st r<g & g in dom f) &
(for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1)
 proof assume A1: f is divergent_in+infty_to+infty;
  assume not (for r ex g st r<g & g in dom f) or
  ex g st for r ex r1 st
  r<r1 & r1 in dom f & g>=f.r1; then consider g such that
  A2: for r ex r1 st r<r1 & r1 in dom f & g>=f.r1 by A1,Def7;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f & g >= f.$2;
  A3: now let n; consider r such that
  A4: n<r & r in dom f & g>=f.r by A2;
   reconsider r as real number;
   take r; thus X[n,r] by A4;
  end; consider s be Real_Sequence such that
  A5: for n holds X[n,s.n] from RealSeqChoice(A3);
 deffunc U(Nat) = $1;
  consider s1 be Real_Sequence such that
  A6: for n holds s1.n=U(n) from ExRealSeq;
  A7: s1 is divergent_to+infty by A6,Th47;
    now let n; n<s.n by A5; hence s1.n<=s.n by A6;end;
  then A8: s is divergent_to+infty by A7,Th69;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A5;
  end; then A9: rng s c=dom f by TARSKI:def 3;
  then f*s is divergent_to+infty by A1,A8,Def7;
  then consider n such that A10: for m st n<=m holds g<(f*s).m by Def4;
    g<(f*s).n by A10; then g<f.(s.n) by A9,RFUNCT_2:21; hence contradiction
by A5
;
 end;
 assume that A11: for r ex g st r<g & g in dom f and
 A12: for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1;
   now let s be Real_Sequence such that
  A13: s is divergent_to+infty & rng s c=dom f;
    now let g; consider r such that
   A14: for r1 st r<r1 & r1 in dom f holds g<f.r1 by A12;
   consider n such that A15: for m st n<=m holds r<s.m by A13,Def4;
   take n; let m; assume n<=m; then A16: r<s.m by A15;
     s.m in rng s by RFUNCT_2:10;
   then g<f.(s.m) by A13,A14,A16; hence g<(f*s).m by A13,RFUNCT_2:21;
  end; hence f*s is divergent_to+infty by Def4;
 end; hence thesis by A11,Def7;
end;

theorem
  f is divergent_in+infty_to-infty iff
 (for r ex g st r<g & g in dom f) &
 for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g
proof thus f is divergent_in+infty_to-infty implies
(for r ex g st r<g & g in dom f) &
(for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g)
 proof assume A1: f is divergent_in+infty_to-infty;
  assume not (for r ex g st r<g & g in dom f) or
  ex g st for r ex r1 st r<r1 & r1 in dom f & f.r1>=g;
  then consider g such that
  A2: for r ex r1 st r<r1 & r1 in dom f & f.r1>=g by A1,Def8;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f & g <= f.$2;
  A3: now let n; consider r such that A4: n<r & r in dom f & f.r>=g by A2;
   reconsider r as real number;
   take r; thus X[n,r] by A4;
  end; consider s be Real_Sequence such that
  A5: for n holds X[n,s.n] from RealSeqChoice(A3);
 deffunc U(Nat) = $1;
  consider s1 be Real_Sequence such that
  A6: for n holds s1.n=U(n) from ExRealSeq;
  A7: s1 is divergent_to+infty by A6,Th47;
    now let n; n<s.n by A5; hence s1.n<=s.n by A6;end;
  then A8: s is divergent_to+infty by A7,Th69;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A5;
  end; then A9: rng s c=dom f by TARSKI:def 3;
  then f*s is divergent_to-infty by A1,A8,Def8;
  then consider n such that A10: for m st n<=m holds (f*s).m<g by Def5;
    (f*s).n<g by A10; then f.(s.n)<g by A9,RFUNCT_2:21;
  hence contradiction by A5
;
 end;
 assume that A11: for r ex g st r<g & g in dom f and
 A12: for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g;
   now let s be Real_Sequence such that
  A13: s is divergent_to+infty & rng s c=dom f;
    now let g; consider r such that
   A14: for r1 st r<r1 & r1 in dom f holds f.r1<g by A12;
   consider n such that A15: for m st n<=m holds r<s.m by A13,Def4;
   take n; let m; assume n<=m; then A16: r<s.m by A15;
     s.m in rng s by RFUNCT_2:10;
   then f.(s.m)<g by A13,A14,A16; hence (f*s).m<g by A13,RFUNCT_2:21;
  end; hence f*s is divergent_to-infty by Def5;
 end; hence thesis by A11,Def8;
end;

theorem
  f is divergent_in-infty_to+infty iff
 (for r ex g st g<r & g in dom f) &
 for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1
proof thus f is divergent_in-infty_to+infty implies
(for r ex g st g<r & g in dom f) &
(for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1)
 proof assume A1: f is divergent_in-infty_to+infty;
  assume not (for r ex g st g<r & g in dom f) or
  ex g st for r ex r1 st r1<r & r1 in dom f & g>=f.r1;
  then consider g such that
  A2: for r ex r1 st r1<r & r1 in dom f & g>=f.r1 by A1,Def10;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f & g >= f.$2;
  A3: now let n; consider r such that
  A4: r<-n & r in dom f & g>=f.r by A2;
   reconsider r as real number;
   take r; thus X[n,r] by A4;
  end; consider s be Real_Sequence such that
  A5: for n holds X[n,s.n] from RealSeqChoice(A3);
 deffunc U(Nat) = -$1;
  consider s1 be Real_Sequence such that
  A6: for n holds s1.n=U(n) from ExRealSeq;
  A7: s1 is divergent_to-infty by A6,Th48;
    now let n; s.n<-n by A5; hence s.n<=s1.n by A6;end;
  then A8: s is divergent_to-infty by A7,Th70;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A5;
  end; then A9: rng s c=dom f by TARSKI:def 3;
  then f*s is divergent_to+infty by A1,A8,Def10;
  then consider n such that A10: for m st n<=m holds g<(f*s).m by Def4;
    g<(f*s).n by A10;
  then g<f.(s.n) by A9,RFUNCT_2:21; hence contradiction by A5;
 end;
 assume that A11: for r ex g st g<r & g in dom f and
 A12: for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1;
   now let s be Real_Sequence such that
  A13: s is divergent_to-infty & rng s c=dom f;
    now let g; consider r such that
   A14: for r1 st r1<r & r1 in dom f holds g<f.r1 by A12;
   consider n such that A15: for m st n<=m holds s.m<r by A13,Def5;
   take n; let m; assume n<=m; then A16: s.m<r by A15;
     s.m in rng s by RFUNCT_2:10;
   then g<f.(s.m) by A13,A14,A16; hence g<(f*s).m by A13,RFUNCT_2:21;
  end; hence f*s is divergent_to+infty by Def4;
 end; hence thesis by A11,Def10;
end;

theorem
  f is divergent_in-infty_to-infty iff
 (for r ex g st g<r & g in dom f) &
 for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g
proof thus f is divergent_in-infty_to-infty implies
(for r ex g st g<r & g in dom f) &
(for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g)
 proof assume A1: f is divergent_in-infty_to-infty;
  assume not (for r ex g st g<r & g in dom f) or
  ex g st for r ex r1 st r1<r & r1 in dom f & f.r1>=g;
  then consider g such that
  A2: for r ex r1 st r1<r & r1 in dom f & f.r1>=g by A1,Def11;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f & g <= f.$2;
  A3: now let n; consider r such that
  A4: r<-n & r in dom f & f.r>=g by A2;
   reconsider r as real number;
   take r; thus X[n,r] by A4;
  end; consider s be Real_Sequence such that
  A5: for n holds X[n,s.n] from RealSeqChoice(A3);
 deffunc U(Nat) = -$1;
  consider s1 be Real_Sequence such that
  A6: for n holds s1.n=U(n) from ExRealSeq;
  A7: s1 is divergent_to-infty by A6,Th48;
    now let n; s.n<-n by A5; hence s.n<=s1.n by A6;end;
  then A8: s is divergent_to-infty by A7,Th70;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A5;
  end; then A9: rng s c=dom f by TARSKI:def 3;
  then f*s is divergent_to-infty by A1,A8,Def11;
  then consider n such that A10: for m st n<=m holds (f*s).m<g by Def5;
    (f*s).n<g by A10;
  then f.(s.n)<g by A9,RFUNCT_2:21; hence contradiction by A5;
 end;
 assume that A11: for r ex g st g<r & g in dom f and
 A12: for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g;
   now let s be Real_Sequence such that
  A13: s is divergent_to-infty & rng s c=dom f;
    now let g; consider r such that
   A14: for r1 st r1<r & r1 in dom f holds f.r1<g by A12;
   consider n such that A15: for m st n<=m holds s.m<r by A13,Def5;
   take n; let m; assume n<=m; then A16: s.m<r by A15;
     s.m in rng s by RFUNCT_2:10;
   then f.(s.m)<g by A13,A14,A16; hence (f*s).m<g by A13,RFUNCT_2:21;
  end; hence f*s is divergent_to-infty by Def5;
 end; hence thesis by A11,Def11;
end;

theorem
  f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty &
(for r ex g st r<g & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in+infty_to+infty & f1(#)f2 is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to+infty &
 f2 is divergent_in+infty_to+infty &
 for r ex g st r<g & g in dom f1/\dom f2;
 A2: now let r; consider g such that A3: r<g & g in dom f1/\dom f2 by A1;
  take g; thus r<g & g in dom(f1+f2) by A3,SEQ_1:def 3;
 end;
   now let seq; assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2);
  then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  then A6: f1*seq is divergent_to+infty by A1,A4,Def7;
    f2*seq is divergent_to+infty by A1,A4,A5,Def7;
  then f1*seq+f2*seq is divergent_to+infty by A6,Th35;
  hence (f1+f2)*seq is divergent_to+infty by A4,A5,RFUNCT_2:23;
 end; hence f1+f2 is divergent_in+infty_to+infty by A2,Def7;
 A7: now let r; consider g such that A8: r<g & g in dom f1/\dom f2 by A1;
  take g; thus r<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
 end;
   now let seq; assume A9: seq is divergent_to+infty & rng seq c=dom(f1(#)
f2);
  then A10: dom(f1(#)f2)=dom f1/\
dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4;
  then A11: f1*seq is divergent_to+infty by A1,A9,Def7;
    f2*seq is divergent_to+infty by A1,A9,A10,Def7;
  then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th37;
  hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23;
 end; hence thesis by A7,Def7;
end;

theorem
  f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty &
(for r ex g st r<g & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in+infty_to-infty & f1(#)f2 is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to-infty &
 f2 is divergent_in+infty_to-infty &
 for r ex g st r<g & g in dom f1/\dom f2;
 A2: now let r; consider g such that A3: r<g & g in dom f1/\dom f2 by A1;
  take g; thus r<g & g in dom(f1+f2) by A3,SEQ_1:def 3;
 end;
   now let seq; assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2);
  then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  then A6: f1*seq is divergent_to-infty by A1,A4,Def8;
    f2*seq is divergent_to-infty by A1,A4,A5,Def8;
  then f1*seq+f2*seq is divergent_to-infty by A6,Th38;
  hence (f1+f2)*seq is divergent_to-infty by A4,A5,RFUNCT_2:23;
 end; hence f1+f2 is divergent_in+infty_to-infty by A2,Def8;
 A7: now let r; consider g such that A8: r<g & g in dom f1/\dom f2 by A1;
  take g; thus r<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
 end;
   now let seq; assume A9: seq is divergent_to+infty & rng seq c=dom(f1(#)
f2);
  then A10: dom(f1(#)f2)=dom f1/\
dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4;
  then A11: f1*seq is divergent_to-infty by A1,A9,Def8;
    f2*seq is divergent_to-infty by A1,A9,A10,Def8;
  then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th51;
  hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23;
 end; hence thesis by A7,Def7;
end;

theorem
  f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty &
(for r ex g st g<r & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in-infty_to+infty & f1(#)f2 is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to+infty &
 f2 is divergent_in-infty_to+infty &
 for r ex g st g<r & g in dom f1/\dom f2;
 A2: now let r; consider g such that A3: g<r & g in dom f1/\dom f2 by A1;
  take g; thus g<r & g in dom(f1+f2) by A3,SEQ_1:def 3;
 end;
   now let seq; assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2);
  then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  then A6: f1*seq is divergent_to+infty by A1,A4,Def10;
    f2*seq is divergent_to+infty by A1,A4,A5,Def10;
  then f1*seq+f2*seq is divergent_to+infty by A6,Th35;
  hence (f1+f2)*seq is divergent_to+infty by A4,A5,RFUNCT_2:23;
 end; hence f1+f2 is divergent_in-infty_to+infty by A2,Def10;
 A7: now let r; consider g such that A8: g<r & g in dom f1/\dom f2 by A1;
  take g; thus g<r & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
 end;
   now let seq; assume A9: seq is divergent_to-infty & rng seq c=dom(f1(#)
f2);
  then A10: dom(f1(#)f2)=dom f1/\
dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4;
  then A11: f1*seq is divergent_to+infty by A1,A9,Def10;
    f2*seq is divergent_to+infty by A1,A9,A10,Def10;
  then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th37;
  hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23;
 end; hence thesis by A7,Def10;
end;

theorem
  f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty &
(for r ex g st g<r & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in-infty_to-infty & f1(#)f2 is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to-infty &
 f2 is divergent_in-infty_to-infty &
 for r ex g st g<r & g in dom f1/\dom f2;
 A2: now let r; consider g such that A3: g<r & g in dom f1/\dom f2 by A1;
  take g; thus g<r & g in dom(f1+f2) by A3,SEQ_1:def 3;
 end;
   now let seq; assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2);
  then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  then A6: f1*seq is divergent_to-infty by A1,A4,Def11;
    f2*seq is divergent_to-infty by A1,A4,A5,Def11;
  then f1*seq+f2*seq is divergent_to-infty by A6,Th38;
  hence (f1+f2)*seq is divergent_to-infty by A4,A5,RFUNCT_2:23;
 end; hence f1+f2 is divergent_in-infty_to-infty by A2,Def11;
 A7: now let r; consider g such that A8: g<r & g in dom f1/\dom f2 by A1;
  take g; thus g<r & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
 end;
   now let seq; assume A9: seq is divergent_to-infty & rng seq c=dom(f1(#)
f2);
  then A10: dom(f1(#)f2)=dom f1/\
dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4;
  then A11: f1*seq is divergent_to-infty by A1,A9,Def11;
    f2*seq is divergent_to-infty by A1,A9,A10,Def11;
  then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th51;
  hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23;
 end; hence thesis by A7,Def10;
end;

theorem
  f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1+f2)) &
(ex r st f2 is_bounded_below_on right_open_halfline(r))
implies f1+f2 is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to+infty &
 for r ex g st r<g & g in dom(f1+f2);
 given r1 such that A2: f2 is_bounded_below_on right_open_halfline(r1);
   now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom(f1+f2);
  then A4: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  consider k such that A5: for n st k<=n holds r1<seq.n by A3,Def4;
    seq^\k is_subsequence_of seq by SEQM_3:47;
  then A6: seq^\k is divergent_to+infty by A3,Th53;
  A7: rng(seq^\k)c=rng seq by RFUNCT_2:7;
  then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1;
  then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def7;
  consider r2 be real number such that
  A10:for g st g in right_open_halfline(r1)/\dom f2 holds r2<=f2.g
   by A2,RFUNCT_1:def 10;
    now let n; A11: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
     k<=n+k by NAT_1:37;
   then r1<seq.(n+k) by A5; then r1<(seq^\k).n by SEQM_3:def 9;
   then (seq^\k).n in {g2: r1<g2};
   then (seq^\k).n in right_open_halfline(r1) by Def3;
   then (seq^\k).n in right_open_halfline(r1)/\dom f2 by A8,A11,XBOOLE_0:def 3
;
   then r2<=f2.((seq^\k).n) by A10; then A12: r2<=(f2*(seq^\k)).n by A8,
RFUNCT_2:21;
     -abs(r2)<=r2 by ABSVALUE:11; then -abs(r2)-1<r2-0 by REAL_1:92;
hence -abs(r2)-1<(f2*(seq^\k)).n by A12,AXIOMS:22;
  end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4;
  then A13: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A9,Th36;
    rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1;
  then f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by RFUNCT_2:23
  .=((f1+f2)*seq)^\k by A3,RFUNCT_2:22;
  hence (f1+f2)*seq is divergent_to+infty by A13,Th34;
 end; hence thesis by A1,Def7;
end;

theorem
  f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & for g st g in dom f2 /\
 right_open_halfline(r1) holds r<=f2.g)
implies f1(#)f2 is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to+infty &
 for r ex g st r<g & g in dom(f1(#)f2);
 given r2,r1 such that
 A2: 0<r2 & for g st g in dom f2/\right_open_halfline(r1) holds r2<=f2.g;
   now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom(f1(#)
f2);
  then A4: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2
by Lm4;
  consider k such that A5: for n st k<=n holds r1<seq.n by A3,Def4;
    seq^\k is_subsequence_of seq by SEQM_3:47;
  then A6: seq^\k is divergent_to+infty by A3,Th53;
  A7: rng(seq^\k)c=rng seq by RFUNCT_2:7;
  then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1;
  then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def7;
    now thus 0<r2 by A2; let n; A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
 k<=n+k by NAT_1:37; then r1<seq.(n+k)
      by A5;
   then r1<(seq^\k).n by SEQM_3:def 9; then (seq^\k).n in {g2: r1<g2};
   then (seq^\k).n in right_open_halfline(r1) by Def3;
   then (seq^\k).n in dom f2/\right_open_halfline(r1) by A8,A10,XBOOLE_0:def 3
;
   then r2<=f2.((seq^\k).n) by A2; hence r2<=(f2*(seq^\k)).n by A8,RFUNCT_2:21;
  end;
  then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty by A9,Th49;
    rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1;
  then (f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by RFUNCT_2:23
  .=((f1(#)f2)*seq)^\k by A3,RFUNCT_2:22;
  hence (f1(#)f2)*seq is divergent_to+infty by A11,Th34;
 end; hence thesis by A1,Def7;
end;

theorem
  f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1+f2)) &
(ex r st f2 is_bounded_below_on left_open_halfline(r))
implies f1+f2 is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to+infty & for r ex g st g<r &
 g in dom(f1+f2);
 given r1 such that A2: f2 is_bounded_below_on left_open_halfline(r1);
   now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom(f1+f2);
  then A4: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  consider k such that A5: for n st k<=n holds seq.n<r1 by A3,Def5;
    seq^\k is_subsequence_of seq by SEQM_3:47;
  then A6: seq^\k is divergent_to-infty by A3,Th54;
  A7: rng(seq^\k)c=rng seq by RFUNCT_2:7;
  then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1;
  then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def10;
  consider r2 be real number such that
  A10:for g st g in left_open_halfline(r1)/\dom f2 holds r2<=f2.g
   by A2,RFUNCT_1:def 10;
    now let n; A11: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; k<=n+k by NAT_1:
37; then seq.(n+k)<r1
      by A5;
   then (seq^\k).n<r1 by SEQM_3:def 9; then (seq^\k).n in {g2: g2<r1};
   then (seq^\k).n in left_open_halfline(r1) by PROB_1:def 15;
   then (seq^\k).n in left_open_halfline(r1)/\dom f2 by A8,A11,XBOOLE_0:def 3;
   then r2<=f2.((seq^\k).n) by A10; then A12: r2<=(f2*(seq^\k)).n by A8,
RFUNCT_2:21;
     -abs(r2)<=r2 by ABSVALUE:11; then -abs(r2)-1<r2-0 by REAL_1:92;
hence -abs(r2)-1<(f2*(seq^\k)).n by A12,AXIOMS:22;
  end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4;
  then A13: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A9,Th36;
    rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1;
  then f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by RFUNCT_2:23
  .=((f1+f2)*seq)^\k by A3,RFUNCT_2:22;
  hence (f1+f2)*seq is divergent_to+infty by A13,Th34;
 end; hence thesis by A1,Def10;
end;

theorem
  f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & for g st g in dom f2 /\ left_open_halfline(r1) holds r<=f2.g)
implies f1(#)f2 is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to+infty &
 for r ex g st g<r & g in dom(f1(#)f2);
 given r2,r1 such that
 A2: 0<r2 & for g st g in dom f2/\left_open_halfline(r1) holds r2<=f2.g;
   now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom(f1(#)
f2);
  then A4: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2
by Lm4;
  consider k such that A5: for n st k<=n holds seq.n<r1 by A3,Def5;
    seq^\k is_subsequence_of seq by SEQM_3:47;
  then A6: seq^\k is divergent_to-infty by A3,Th54;
  A7: rng(seq^\k)c=rng seq by RFUNCT_2:7;
  then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1;
  then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def10;
    now thus 0<r2 by A2; let n; A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
     k<=n+k by NAT_1:37
; then seq.(n+k)<r1 by A5; then (seq^\k).n<r1 by SEQM_3:def 9;
   then (seq^\k).n in {g2: g2<r1};
   then (seq^\k).n in left_open_halfline(r1) by PROB_1:def 15;
   then (seq^\k).n in dom f2/\left_open_halfline(r1) by A8,A10,XBOOLE_0:def 3;
   then r2<=f2.((seq^\k).n) by A2; hence r2<=(f2*(seq^\k)).n by A8,RFUNCT_2:21
;
  end;
  then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty by A9,Th49;
    rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1;
  then (f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by RFUNCT_2:23
  .=((f1(#)f2)*seq)^\k by A3,RFUNCT_2:22;
  hence (f1(#)f2)*seq is divergent_to+infty by A11,Th34;
 end; hence thesis by A1,Def10;
end;

theorem
  (f is divergent_in+infty_to+infty & r>0 implies
   r(#)f is divergent_in+infty_to+infty) &
(f is divergent_in+infty_to+infty & r<0 implies
   r(#)f is divergent_in+infty_to-infty) &
(f is divergent_in+infty_to-infty & r>0 implies
   r(#)f is divergent_in+infty_to-infty) &
(f is divergent_in+infty_to-infty & r<0 implies
   r(#)f is divergent_in+infty_to+infty)
proof
thus f is divergent_in+infty_to+infty & r>0 implies
   r(#)f is divergent_in+infty_to+infty
 proof assume A1: f is divergent_in+infty_to+infty & r>0;
  A2: now let r1; consider g such that A3: r1<g & g in dom f by A1,Def7;
  take g; thus r1<g & g in dom(r(#)f) by A3,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f);
   then A4: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to+infty by A1,Def7;
   then r(#)(f*seq) is divergent_to+infty by A1,Th40;
   hence (r(#)f)*seq is divergent_to+infty by A4,RFUNCT_2:24;
  end; hence thesis by A2,Def7;
 end;
thus f is divergent_in+infty_to+infty & r<0 implies
   r(#)f is divergent_in+infty_to-infty
 proof assume A5: f is divergent_in+infty_to+infty & r<0;
  A6: now let r1; consider g such that A7: r1<g & g in dom f by A5,Def7;
  take g; thus r1<g & g in dom(r(#)f) by A7,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f);
   then A8: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to+infty by A5,Def7;
   then r(#)(f*seq) is divergent_to-infty by A5,Th40;
   hence (r(#)f)*seq is divergent_to-infty by A8,RFUNCT_2:24;
  end; hence thesis by A6,Def8;
 end;
thus f is divergent_in+infty_to-infty & r>0 implies
   r(#)f is divergent_in+infty_to-infty
 proof assume A9: f is divergent_in+infty_to-infty & r>0;
  A10: now let r1; consider g such that A11: r1<g & g in dom f by A9,Def8;
  take g; thus r1<g & g in dom(r(#)f) by A11,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f);
   then A12: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to-infty by A9,Def8;
   then r(#)(f*seq) is divergent_to-infty by A9,Th41;
   hence (r(#)f)*seq is divergent_to-infty by A12,RFUNCT_2:24;
  end; hence thesis by A10,Def8;
 end;
 assume A13: f is divergent_in+infty_to-infty & r<0;
 A14: now let r1; consider g such that A15: r1<g & g in dom f by A13,Def8;
  take g; thus r1<g & g in dom(r(#)f) by A15,SEQ_1:def 6;
 end;
   now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f);
  then A16: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6;
  then f*seq is divergent_to-infty by A13,Def8;
  then r(#)(f*seq) is divergent_to+infty by A13,Th41;
  hence (r(#)f)*seq is divergent_to+infty by A16,RFUNCT_2:24;
 end; hence thesis by A14,Def7;
end;

theorem
  (f is divergent_in-infty_to+infty & r>0 implies
   r(#)f is divergent_in-infty_to+infty) &
(f is divergent_in-infty_to+infty & r<0 implies
   r(#)f is divergent_in-infty_to-infty) &
(f is divergent_in-infty_to-infty & r>0 implies
   r(#)f is divergent_in-infty_to-infty) &
(f is divergent_in-infty_to-infty & r<0 implies
   r(#)f is divergent_in-infty_to+infty)
proof
thus f is divergent_in-infty_to+infty & r>0 implies
   r(#)f is divergent_in-infty_to+infty
 proof assume A1: f is divergent_in-infty_to+infty & r>0;
  A2: now let r1; consider g such that A3: g<r1 & g in dom f by A1,Def10;
  take g; thus g<r1 & g in dom(r(#)f) by A3,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f);
   then A4: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to+infty by A1,Def10;
   then r(#)(f*seq) is divergent_to+infty by A1,Th40;
   hence (r(#)f)*seq is divergent_to+infty by A4,RFUNCT_2:24;
  end; hence thesis by A2,Def10;
 end;
thus f is divergent_in-infty_to+infty & r<0 implies
   r(#)f is divergent_in-infty_to-infty
 proof assume A5: f is divergent_in-infty_to+infty & r<0;
  A6: now let r1; consider g such that A7: g<r1 & g in dom f by A5,Def10;
  take g; thus g<r1 & g in dom(r(#)f) by A7,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f);
   then A8: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to+infty by A5,Def10;
   then r(#)(f*seq) is divergent_to-infty by A5,Th40;
   hence (r(#)f)*seq is divergent_to-infty by A8,RFUNCT_2:24;
  end; hence thesis by A6,Def11;
 end;
thus f is divergent_in-infty_to-infty & r>0 implies
   r(#)f is divergent_in-infty_to-infty
 proof assume A9: f is divergent_in-infty_to-infty & r>0;
  A10: now let r1; consider g such that A11: g<r1 & g in dom f by A9,Def11;
  take g; thus g<r1 & g in dom(r(#)f) by A11,SEQ_1:def 6;
  end;
    now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f);
   then A12: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6;
   then f*seq is divergent_to-infty by A9,Def11;
   then r(#)(f*seq) is divergent_to-infty by A9,Th41;
   hence (r(#)f)*seq is divergent_to-infty by A12,RFUNCT_2:24;
  end; hence thesis by A10,Def11;
 end;
 assume A13: f is divergent_in-infty_to-infty & r<0;
 A14: now let r1; consider g such that A15: g<r1 & g in dom f by A13,Def11;
  take g; thus g<r1 & g in dom(r(#)f) by A15,SEQ_1:def 6;
 end;
   now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f);
  then A16: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6;
  then f*seq is divergent_to-infty by A13,Def11;
  then r(#)(f*seq) is divergent_to+infty by A13,Th41;
  hence (r(#)f)*seq is divergent_to+infty by A16,RFUNCT_2:24;
 end; hence thesis by A14,Def10;
end;

theorem
  (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty)
implies
abs(f) is divergent_in+infty_to+infty
proof assume A1: f is divergent_in+infty_to+infty or
  f is divergent_in+infty_to-infty;
   now per cases by A1;
 suppose A2: f is divergent_in+infty_to+infty;
  A3: now let r; consider g such that A4: r<g & g in dom f by A2,Def7; take g;
   thus r<g & g in dom abs(f) by A4,SEQ_1:def 10;
  end;
    now let seq;
  assume A5: seq is divergent_to+infty & rng seq c=dom abs(f);
   then A6: rng seq c=dom f by SEQ_1:def 10
; then f*seq is divergent_to+infty by A2,A5,Def7;
   then abs(f*seq) is divergent_to+infty by Th52;
   hence abs(f)*seq is divergent_to+infty by A6,RFUNCT_2:25;
  end; hence thesis by A3,Def7;
 suppose A7: f is divergent_in+infty_to-infty;
  A8: now let r; consider g such that A9: r<g & g in dom f by A7,Def8; take g;
   thus r<g & g in dom abs(f) by A9,SEQ_1:def 10;
  end;
    now let seq; assume A10: seq is divergent_to+infty & rng seq c=dom abs(f);
   then A11: rng seq c=dom f by SEQ_1:def 10
; then f*seq is divergent_to-infty by A7,A10,Def8;
   then abs(f*seq) is divergent_to+infty by Th52;
   hence abs(f)*seq is divergent_to+infty by A11,RFUNCT_2:25;
  end; hence thesis by A8,Def7;
 end; hence thesis;
end;

theorem
  (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty)
implies
abs(f) is divergent_in-infty_to+infty
proof assume A1: f is divergent_in-infty_to+infty or
  f is divergent_in-infty_to-infty;
   now per cases by A1;
 suppose A2: f is divergent_in-infty_to+infty;
  A3: now let r; consider g such that A4: g<r & g in dom f by A2,Def10; take g;
   thus g<r & g in dom abs(f) by A4,SEQ_1:def 10;
  end;
    now let seq;
  assume A5: seq is divergent_to-infty & rng seq c=dom abs(f);
   then A6: rng seq c=dom f by SEQ_1:def 10
; then f*seq is divergent_to+infty by A2,A5,Def10;
   then abs(f*seq) is divergent_to+infty by Th52;
   hence abs(f)*seq is divergent_to+infty by A6,RFUNCT_2:25;
  end; hence thesis by A3,Def10;
 suppose A7: f is divergent_in-infty_to-infty;
  A8: now let r; consider g such that A9: g<r & g in dom f by A7,Def11; take g;
   thus g<r & g in dom abs(f) by A9,SEQ_1:def 10;
  end;
    now let seq; assume A10: seq is divergent_to-infty & rng seq c=dom abs(f);
   then A11: rng seq c=dom f by SEQ_1:def 10
; then f*seq is divergent_to-infty by A7,A10,Def11;
   then abs(f*seq) is divergent_to+infty by Th52;
   hence abs(f)*seq is divergent_to+infty by A11,RFUNCT_2:25;
  end; hence thesis by A8,Def10;
 end; hence thesis;
end;

theorem Th95:
(ex r st f is_non_decreasing_on right_open_halfline(r) &
not f is_bounded_above_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty
proof given r1 such that A1: f is_non_decreasing_on right_open_halfline(r1) &
 not f is_bounded_above_on right_open_halfline(r1);
 assume A2: for r ex g st r<g & g in dom f;
   now let seq such that A3: seq is divergent_to+infty & rng seq c=dom f;
    now let r; consider g1 such that
   A4: g1 in right_open_halfline(r1)/\dom f & r<f.g1 by A1,RFUNCT_1:def 9;
   consider n such that
   A5: for m st n<=m holds abs(g1)+abs(r1)<seq.m by A3,Def4;
   take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m;
   then A7: abs(g1)+abs(r1)<seq.m by A5; A8: r1<=abs(r1) by ABSVALUE:11;
     0<=abs(g1) by ABSVALUE:5; then 0+r1<=abs(g1)+abs(r1) by A8,REAL_1:55;
then r1<seq.m by A7,AXIOMS:22;
   then seq.m in {g2: r1<g2}; then seq.m in right_open_halfline(r1) by Def3;
   then A9: seq.m in right_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3;
   A10: g1<=abs(g1) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
   then g1+0<=abs(g1)+abs(r1) by A10,REAL_1:55;
   then g1<seq.m by A7,AXIOMS:22; then f.g1<=f.(seq.m) by A1,A4,A9,RFUNCT_2:def
4
;
   then r<f.(seq.m) by A4,AXIOMS:22; hence r<(f*seq).m by A3,RFUNCT_2:21;
  end; hence f*seq is divergent_to+infty by Def4;
 end; hence thesis by A2,Def7;
end;

theorem
  (ex r st f is_increasing_on right_open_halfline(r) &
not f is_bounded_above_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty
proof given r such that A1: f is_increasing_on right_open_halfline(r) &
 not f is_bounded_above_on right_open_halfline(r);
 assume A2: for r ex g st r<g & g in dom f;
   f is_non_decreasing_on right_open_halfline(r) by A1,RFUNCT_2:55;
 hence thesis by A1,A2,Th95;
end;

theorem Th97:
(ex r st f is_non_increasing_on right_open_halfline(r) &
not f is_bounded_below_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty
proof given r1 such that A1: f is_non_increasing_on right_open_halfline(r1) &
 not f is_bounded_below_on right_open_halfline(r1);
 assume A2: for r ex g st r<g & g in dom f;
   now let seq such that A3: seq is divergent_to+infty & rng seq c=dom f;
    now let r; consider g1 such that
   A4: g1 in right_open_halfline(r1)/\dom f & f.g1<r by A1,RFUNCT_1:def 10;
   consider n such that
   A5: for m st n<=m holds abs(g1)+abs(r1)<seq.m by A3,Def4;
   take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m;
   then A7: abs(g1)+abs(r1)<seq.m by A5; A8: r1<=abs(r1) by ABSVALUE:11;
     0<=abs(g1) by ABSVALUE:5; then 0+r1<=abs(g1)+abs(r1) by A8,REAL_1:55;
then r1<seq.m by A7,AXIOMS:22;
   then seq.m in {g2: r1<g2}; then seq.m in right_open_halfline(r1) by Def3;
   then A9: seq.m in right_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3;
   A10: g1<=abs(g1) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
   then g1+0<=abs(g1)+abs(r1) by A10,REAL_1:55;
   then g1<seq.m by A7,AXIOMS:22; then f.(seq.m)<=f.g1 by A1,A4,A9,RFUNCT_2:def
5
;
   then f.(seq.m)<r by A4,AXIOMS:22; hence (f*seq).m<r by A3,RFUNCT_2:21;
  end; hence f*seq is divergent_to-infty by Def5;
 end; hence thesis by A2,Def8;
end;

theorem
  (ex r st f is_decreasing_on right_open_halfline(r) &
not f is_bounded_below_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty
proof given r such that A1: f is_decreasing_on right_open_halfline(r) &
 not f is_bounded_below_on right_open_halfline(r);
 assume A2: for r ex g st r<g & g in dom f;
   f is_non_increasing_on right_open_halfline(r) by A1,RFUNCT_2:56;
 hence thesis by A1,A2,Th97;
end;

theorem Th99:
(ex r st f is_non_increasing_on left_open_halfline(r) &
not f is_bounded_above_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty
proof given r1 such that A1: f is_non_increasing_on left_open_halfline(r1) &
 not f is_bounded_above_on left_open_halfline(r1);
 assume A2: for r ex g st g<r & g in dom f;
   now let seq such that A3: seq is divergent_to-infty & rng seq c=dom f;
    now let r; consider g1 such that
   A4: g1 in left_open_halfline(r1)/\dom f & r<f.g1 by A1,RFUNCT_1:def 9;
   consider n such that
   A5: for m st n<=m holds seq.m<-abs(r1)-abs(g1) by A3,Def5;
   take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m;
   then A7: seq.m<-abs(r1)-abs(g1) by A5; A8: -abs(r1)<=r1 by ABSVALUE:11;
     0<=abs(g1) by ABSVALUE:5; then -abs(r1)-abs(g1)<=r1-0 by A8,REAL_1:92;
then seq.m<r1 by A7,AXIOMS:22;
   then seq.m in {g2: g2<r1};
   then seq.m in left_open_halfline(r1) by PROB_1:def 15;
   then A9: seq.m in left_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3;
   A10: -abs(g1)<=g1 by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
   then -abs(g1)-abs(r1)<=g1-0 by A10,REAL_1:92;
then -abs(r1)+-abs(g1)<=g1 by XCMPLX_0:def 8;
   then -abs(r1)-abs(g1)<=g1 by XCMPLX_0:def 8; then seq.m<g1 by A7,AXIOMS:22
;
   then f.g1<=
f.(seq.m) by A1,A4,A9,RFUNCT_2:def 5; then r<f.(seq.m) by A4,AXIOMS:22;
   hence r<(f*seq).m by A3,RFUNCT_2:21;
  end; hence f*seq is divergent_to+infty by Def4;
 end; hence thesis by A2,Def10;
end;

theorem
  (ex r st f is_decreasing_on left_open_halfline(r) &
not f is_bounded_above_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty
proof given r such that A1: f is_decreasing_on left_open_halfline(r) &
 not f is_bounded_above_on left_open_halfline(r);
 assume A2: for r ex g st g<r & g in dom f;
   f is_non_increasing_on left_open_halfline(r) by A1,RFUNCT_2:56;
 hence thesis by A1,A2,Th99;
end;

theorem Th101:
(ex r st f is_non_decreasing_on left_open_halfline(r) &
not f is_bounded_below_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty
proof given r1 such that A1: f is_non_decreasing_on left_open_halfline(r1) &
 not f is_bounded_below_on left_open_halfline(r1);
 assume A2: for r ex g st g<r & g in dom f;
   now let seq such that A3: seq is divergent_to-infty & rng seq c=dom f;
    now let r; consider g1 such that
   A4: g1 in left_open_halfline(r1)/\dom f & f.g1<r by A1,RFUNCT_1:def 10;
   consider n such that
   A5: for m st n<=m holds seq.m<-abs(r1)-abs(g1) by A3,Def5;
   take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m;
   then A7: seq.m<-abs(r1)-abs(g1) by A5; A8: -abs(r1)<=r1 by ABSVALUE:11;
     0<=abs(g1) by ABSVALUE:5; then -abs(r1)-abs(g1)<=r1-0 by A8,REAL_1:92;
then seq.m<r1 by A7,AXIOMS:22;
   then seq.m in {g2: g2<r1};
   then seq.m in left_open_halfline(r1) by PROB_1:def 15;
   then A9: seq.m in left_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3;
   A10: -abs(g1)<=g1 by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
   then -abs(g1)-abs(r1)<=g1-0 by A10,REAL_1:92;
then -abs(r1)+-abs(g1)<=g1 by XCMPLX_0:def 8;
   then -abs(r1)-abs(g1)<=g1 by XCMPLX_0:def 8;
   then seq.m<g1 by A7,AXIOMS:22;
   then f.(seq.m)<=
f.g1 by A1,A4,A9,RFUNCT_2:def 4; then f.(seq.m)<r by A4,AXIOMS:22;
   hence (f*seq).m<r by A3,RFUNCT_2:21;
  end; hence f*seq is divergent_to-infty by Def5;
 end; hence thesis by A2,Def11;
end;

theorem
  (ex r st f is_increasing_on left_open_halfline(r) &
not f is_bounded_below_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty
proof given r such that A1: f is_increasing_on left_open_halfline(r) &
 not f is_bounded_below_on left_open_halfline(r);
 assume A2: for r ex g st g<r & g in dom f;
   f is_non_decreasing_on left_open_halfline(r) by A1,RFUNCT_2:55;
 hence thesis by A1,A2,Th101;
end;

theorem Th103:
f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom f) &
(ex r st dom f /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
 for g st g in dom f /\ right_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to+infty &
  for r ex g st r<g & g in dom f;
 given r1 such that A2: dom f/\right_open_halfline(r1)c=
 dom f1/\right_open_halfline(r1) &
 for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g;
   now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom f;
  then consider k such that A4: for n st k<=n holds r1<seq.n by Def4;
    rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3,
XBOOLE_1:1;
    now let x be set; assume x in rng(seq^\k); then consider n such that
   A6: (seq^\k).n=x by RFUNCT_2:9;
     k<=n+k by NAT_1:37; then r1<seq.(n+k) by A4;
   then r1<(seq^\k).n by SEQM_3:def 9; then x in {g2: r1<g2} by A6;
   hence x in right_open_halfline(r1) by Def3;
  end; then rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3;
 then A7: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A5,XBOOLE_1:19;
 then A8: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A2,XBOOLE_1:1;
   dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
 then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1;
   seq^\k is_subsequence_of seq by SEQM_3:47;
 then seq^\k is divergent_to+infty by A3,Th53;
 then A10: f1*(seq^\k) is divergent_to+infty by A1,A9,Def7;
   now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
  then f1.((seq^\k).n)<=f.((seq^\k).n) by A2,A7;
  then (f1*(seq^\k)).n<=f.((seq^\k).n) by A9,RFUNCT_2:21;
  hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A5,RFUNCT_2:21;
 end; then A11: f*(seq^\k) is divergent_to+infty by A10,Th69;
   f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22;
 hence f*seq is divergent_to+infty by A11,Th34;
 end; hence f is divergent_in+infty_to+infty by A1,Def7;
end;

theorem Th104:
f1 is divergent_in+infty_to-infty & (for r ex g st r<g & g in dom f) &
(ex r st dom f/\right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
 for g st g in dom f /\ right_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in+infty_to-infty
proof assume A1: f1 is divergent_in+infty_to-infty &
  for r ex g st r<g & g in dom f;
 given r1 such that A2: dom f/\right_open_halfline(r1)c=
 dom f1/\right_open_halfline(r1) &
 for g st g in dom f/\right_open_halfline(r1) holds f.g<=f1.g;
   now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom f;
  then consider k such that A4: for n st k<=n holds r1<seq.n by Def4;
    rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3,
XBOOLE_1:1;
    now let x be set; assume x in rng(seq^\k); then consider n such that
   A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
   then r1<seq.(n+k) by A4;
   then r1<(seq^\k).n by SEQM_3:def 9; then x in {g2: r1<g2}
      by A6;
   hence x in right_open_halfline(r1) by Def3;
  end; then rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3;
 then A7: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A5,XBOOLE_1:19;
 then A8: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A2,XBOOLE_1:1;
   dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
 then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1;
   seq^\k is_subsequence_of seq by SEQM_3:47;
 then seq^\k is divergent_to+infty by A3,Th53;
 then A10: f1*(seq^\k) is divergent_to-infty by A1,A9,Def8;
   now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
  then f.((seq^\k).n)<=f1.((seq^\k).n) by A2,A7;
  then (f*(seq^\k)).n<=f1.((seq^\k).n) by A5,RFUNCT_2:21;
  hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A9,RFUNCT_2:21;
 end; then A11: f*(seq^\k) is divergent_to-infty by A10,Th70;
   f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22;
 hence f*seq is divergent_to-infty by A11,Th34;
 end; hence f is divergent_in+infty_to-infty by A1,Def8;
end;

theorem Th105:
f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom f) &
(ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
 for g st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to+infty &
  for r ex g st g<r & g in dom f;
 given r1 such that A2: dom f/\left_open_halfline(r1)c=
 dom f1/\left_open_halfline(r1) &
 for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g;
   now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom f;
  then consider k such that A4: for n st k<=n holds seq.n<r1 by Def5;
    rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3,
XBOOLE_1:1;
    now let x be set; assume x in rng(seq^\k); then consider n such that
   A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
   then seq.(n+k)<r1 by A4;
   then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g2: g2<r1}
      by A6;
   hence x in left_open_halfline(r1) by PROB_1:def 15;
  end; then rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3;
 then A7: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A5,XBOOLE_1:19;
 then A8: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A2,XBOOLE_1:1;
   dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
 then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1;
   seq^\k is_subsequence_of seq by SEQM_3:47;
 then seq^\k is divergent_to-infty by A3,Th54;
 then A10: f1*(seq^\k) is divergent_to+infty by A1,A9,Def10;
   now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
  then f1.((seq^\k).n)<=f.((seq^\k).n) by A2,A7;
  then (f1*(seq^\k)).n<=f.((seq^\k).n) by A9,RFUNCT_2:21;
  hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A5,RFUNCT_2:21;
 end; then A11: f*(seq^\k) is divergent_to+infty by A10,Th69;
   f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22;
 hence f*seq is divergent_to+infty by A11,Th34;
 end; hence f is divergent_in-infty_to+infty by A1,Def10;
end;

theorem Th106:
f1 is divergent_in-infty_to-infty & (for r ex g st g<r & g in dom f) &
(ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
 for g st g in dom f /\ left_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in-infty_to-infty
proof assume A1: f1 is divergent_in-infty_to-infty &
  for r ex g st g<r & g in dom f;
 given r1 such that A2: dom f/\left_open_halfline(r1)c=
 dom f1/\left_open_halfline(r1) &
 for g st g in dom f/\left_open_halfline(r1) holds f.g<=f1.g;
   now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom f;
  then consider k such that A4: for n st k<=n holds seq.n<r1 by Def5;
    rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3,
XBOOLE_1:1;
    now let x be set; assume x in rng(seq^\k); then consider n such that
   A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
   then seq.(n+k)<r1 by A4;
   then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g2: g2<r1}
      by A6;
   hence x in left_open_halfline(r1) by PROB_1:def 15;
  end; then rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3;
 then A7: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A5,XBOOLE_1:19;
 then A8: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A2,XBOOLE_1:1;
   dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
 then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1;
   seq^\k is_subsequence_of seq by SEQM_3:47;
 then seq^\k is divergent_to-infty by A3,Th54;
 then A10: f1*(seq^\k) is divergent_to-infty by A1,A9,Def11;
   now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
  then f.((seq^\k).n)<=f1.((seq^\k).n) by A2,A7;
  then (f*(seq^\k)).n<=f1.((seq^\k).n) by A5,RFUNCT_2:21;
  hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A9,RFUNCT_2:21;
 end; then A11: f*(seq^\k) is divergent_to-infty by A10,Th70;
   f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22;
 hence f*seq is divergent_to-infty by A11,Th34;
 end; hence f is divergent_in-infty_to-infty by A1,Def11;
end;

theorem
  f1 is divergent_in+infty_to+infty &
(ex r st right_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in right_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in+infty_to+infty
proof assume A1: f1 is divergent_in+infty_to+infty; given r1 such that
 A2: right_open_halfline(r1)c=dom f/\dom f1 &
  for g st g in right_open_halfline(r1) holds f1.g<=f.g;
 A3: now let r; consider g being real number such that
   A4: abs(r)+abs(r1)<g by REAL_1:76;
  reconsider g as Real by XREAL_0:def 1;
  take g; A5: 0<=abs(r1) by ABSVALUE:5; r<=abs(r) by ABSVALUE:11;
  then 0+r<=abs(r)+abs(r1) by A5,REAL_1:55;
  hence r<g by A4,AXIOMS:22;
  A6: 0<=abs(r) by ABSVALUE:5; r1<=abs(r1) by ABSVALUE:11;
  then 0+r1<=abs(r)+abs(r1) by A6,REAL_1:55;
  then r1<g by A4,AXIOMS:22; then g in {g2: r1<g2};
  then g in right_open_halfline(r1) by Def3; hence g in dom f by A2,XBOOLE_0:
def 3;
 end;
   now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then A7: right_open_halfline(r1)c=dom f & right_open_halfline(r1) c=dom f1
   by A2,XBOOLE_1:1;
  then A8: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1:
28;
  hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by A7,
XBOOLE_1:28;
  let g; assume g in dom f/\right_open_halfline(r1); hence f1.g<=f.g by A2,A8
;
 end; hence thesis by A1,A3,Th103;
end;

theorem
  f1 is divergent_in+infty_to-infty & (ex r st
 right_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in right_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in+infty_to-infty
proof assume A1: f1 is divergent_in+infty_to-infty; given r1 such that
 A2: right_open_halfline(r1)c=dom f/\dom f1 &
  for g st g in right_open_halfline(r1) holds f.g<=f1.g;
 A3: now let r; consider g being real number such that
 A4: abs(r)+abs(r1)<g by REAL_1:76;
  reconsider g as Real by XREAL_0:def 1;
  take g; A5: 0<=abs(r1) by ABSVALUE:5; r<=abs(r) by ABSVALUE:11;
  then 0+r<=abs(r)+abs(r1) by A5,REAL_1:55;
  hence r<g by A4,AXIOMS:22;
  A6: 0<=abs(r) by ABSVALUE:5; r1<=abs(r1) by ABSVALUE:11;
  then 0+r1<=abs(r)+abs(r1) by A6,REAL_1:55;
  then r1<g by A4,AXIOMS:22; then g in {g2: r1<g2};
  then g in right_open_halfline(r1) by Def3; hence g in dom f by A2,XBOOLE_0:
def 3;
 end;
   now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then A7: right_open_halfline(r1)c=dom f & right_open_halfline(r1) c=dom f1
   by A2,XBOOLE_1:1;
  then A8: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1:
28;
  hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by A7,
XBOOLE_1:28;
  let g; assume g in dom f/\right_open_halfline(r1); hence f.g<=f1.g by A2,A8
;
 end; hence thesis by A1,A3,Th104;
end;

theorem
  f1 is divergent_in-infty_to+infty & (ex r st
 left_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in left_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in-infty_to+infty
proof assume A1: f1 is divergent_in-infty_to+infty; given r1 such that
 A2: left_open_halfline(r1)c=dom f/\dom f1 &
  for g st g in left_open_halfline(r1) holds f1.g<=f.g;
 A3: now let r; consider g being real number such that
 A4: g<-abs(r)-abs(r1) by REAL_1:77;
  reconsider g as Real by XREAL_0:def 1;
  take g; A5: 0<=abs(r1) by ABSVALUE:5; -abs(r)<=r by ABSVALUE:11;
  then -abs(r)-abs(r1)<=r-0 by A5,REAL_1:92; hence g<r by A4,AXIOMS:22;
  A6: 0<=abs(r) by ABSVALUE:5; -abs(r1)<=r1 by ABSVALUE:11;
  then -abs(r1)-abs(r)<=r1-0 by A6,REAL_1:92;
then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8;
  then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A4,AXIOMS:22;
  then g in {g2: g2<r1}; then g in left_open_halfline(r1) by PROB_1:def 15;
hence g in dom f by A2,XBOOLE_0:def 3;
 end;
   now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then A7: left_open_halfline(r1)c=dom f & left_open_halfline(r1) c=dom f1
   by A2,XBOOLE_1:1;
  then A8: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1:28;
  hence dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A7,
XBOOLE_1:28;
  let g; assume g in dom f/\left_open_halfline(r1); hence f1.g<=f.g by A2,A8;
 end; hence thesis by A1,A3,Th105;
end;

theorem
  f1 is divergent_in-infty_to-infty & (ex r st
 left_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in left_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in-infty_to-infty
proof assume A1: f1 is divergent_in-infty_to-infty; given r1 such that
 A2: left_open_halfline(r1)c=dom f/\dom f1 &
  for g st g in left_open_halfline(r1) holds f.g<=f1.g;
 A3: now let r; consider g being real number such that
 A4: g<-abs(r)-abs(r1) by REAL_1:77;
  reconsider g as Real by XREAL_0:def 1;
  take g; A5: 0<=abs(r1) by ABSVALUE:5; -abs(r)<=r by ABSVALUE:11;
  then -abs(r)-abs(r1)<=r-0 by A5,REAL_1:92; hence g<r by A4,AXIOMS:22;
  A6: 0<=abs(r) by ABSVALUE:5; -abs(r1)<=r1 by ABSVALUE:11;
  then -abs(r1)-abs(r)<=r1-0 by A6,REAL_1:92;
then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8;
  then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A4,AXIOMS:22;
  then g in {g2: g2<r1}; then g in left_open_halfline(r1) by PROB_1:def 15;
hence g in dom f by A2,XBOOLE_0:def 3;
 end;
   now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
  then A7: left_open_halfline(r1)c=dom f & left_open_halfline(r1) c=dom f1
   by A2,XBOOLE_1:1;
  then A8: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1:28;
  hence dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A7,
XBOOLE_1:28;
  let g; assume g in dom f/\left_open_halfline(r1); hence f.g<=f1.g by A2,A8;
 end; hence thesis by A1,A3,Th106;
end;

definition let f;
assume A1: f is convergent_in+infty;
func lim_in+infty f ->Real means :Def12:
for seq st seq is divergent_to+infty & rng seq c= dom f holds
f*seq is convergent & lim(f*seq)=it;
existence by A1,Def6;
uniqueness
proof let g1,g2 such that
 A2: for seq st seq is divergent_to+infty & rng seq c= dom f holds
 f*seq is convergent & lim(f*seq)=g1 and
 A3: for seq st seq is divergent_to+infty & rng seq c= dom f holds
 f*seq is convergent & lim(f*seq)=g2;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f;
 A4: now let n; consider g such that A5: n<g & g in dom f by A1,Def6;
   reconsider g as real number;
  take g; thus X[n,g] by A5;
 end;
 consider s1 be Real_Sequence such that
 A6: for n holds X[n,s1.n] from RealSeqChoice(A4);
 deffunc U(Nat) = $1;
 consider s2 be Real_Sequence such that
 A7: for n holds s2.n=U(n) from ExRealSeq;
 A8: s2 is divergent_to+infty by A7,Th47;
    now let n; n<s1.n by A6; hence s2.n<=s1.n by A7;
  end;
 then A9: s1 is divergent_to+infty by A8,Th69;
 A10: rng s1 c= dom f
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; hence x in dom f by A6;
 end; then lim(f*s1)=g1 by A2,A9; hence g1=g2 by A3,A9,A10;
end;
end;

definition let f;
assume A1: f is convergent_in-infty;
func lim_in-infty f ->Real means :Def13:
for seq st seq is divergent_to-infty & rng seq c= dom f holds
f*seq is convergent & lim(f*seq)=it;
existence by A1,Def9;
uniqueness
proof let g1,g2 such that
 A2: for seq st seq is divergent_to-infty & rng seq c= dom f holds
 f*seq is convergent & lim(f*seq)=g1 and
 A3: for seq st seq is divergent_to-infty & rng seq c= dom f holds
 f*seq is convergent & lim(f*seq)=g2;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f;
 A4: now let n; consider g such that A5: g<-n & g in dom f by A1,Def9;
   reconsider g as real number;
  take g; thus X[n,g] by A5;
 end;
 consider s1 be Real_Sequence such that
 A6: for n holds X[n,s1.n] from RealSeqChoice(A4);
 deffunc U(Nat) = -$1;
 consider s2 be Real_Sequence such that
 A7: for n holds s2.n=U(n) from ExRealSeq;
 A8: s2 is divergent_to-infty by A7,Th48;
    now let n; s1.n<-n by A6; hence s1.n<=s2.n by A7;
  end;
 then A9: s1 is divergent_to-infty by A8,Th70;
 A10: rng s1 c= dom f
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; hence x in dom f by A6;
 end; then lim(f*s1)=g1 by A2,A9; hence g1=g2 by A3,A9,A10;
end;
end;

canceled 2;

theorem
  f is convergent_in-infty implies (lim_in-infty f=g iff
for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1)
proof assume A1: f is convergent_in-infty;
thus lim_in-infty f=g implies
for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1
 proof assume A2: lim_in-infty f=g;
  given g1 such that
  A3: 0<g1 & for r ex r1 st r1<r & r1 in dom f & abs(f.r1-g)>=g1;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f & abs(f.$2-g)>=g1;
  A4: now let n; consider r such that
  A5: r<-n & r in dom f & abs(f.r-g)>=g1 by A3;
   reconsider r as real number;
   take r; thus X[n,r] by A5;
  end; consider s be Real_Sequence such that
  A6: for n holds X[n,s.n] from RealSeqChoice(A4);
 deffunc U(Nat) = -$1;
  consider s1 be Real_Sequence such that
  A7: for n holds s1.n=U(n) from ExRealSeq;
  A8: s1 is divergent_to-infty by A7,Th48;
    now let n; s.n<-n by A6; hence s.n<=s1.n by A7;end;
  then A9: s is divergent_to-infty by A8,Th70;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A6;
  end; then A10: rng s c=dom f by TARSKI:def 3;
  then f*s is convergent & lim(f*s)=g by A1,A2,A9,Def13;
  then consider n such that A11: for m st n<=m holds abs((f*s).m-g)<g1 by A3,
SEQ_2:def 7;
    abs((f*s).n-g)<g1 by A11; then abs(f.(s.n)-g)<g1 by A10,RFUNCT_2:21;
  hence contradiction by A6;
 end;
 assume A12: for g1 st 0<g1 ex r st
 for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1;
   now let s be Real_Sequence such that
  A13: s is divergent_to-infty & rng s c=dom f;
  A14: now let g1 be real number;
A15:  g1 is Real by XREAL_0:def 1;
  assume 0<g1; then consider r such that
   A16: for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 by A12,A15;
   consider n such that A17: for m st n<=m holds s.m<r by A13,Def5;
   take n; let m; assume n<=m; then A18: s.m<r by A17;
     s.m in rng s by RFUNCT_2:10;
   then abs(f.(s.m)-g)<g1 by A13,A16,A18;
   hence abs((f*s).m-g)<g1 by A13,RFUNCT_2:21;
  end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A14,SEQ_2:
def 7;
 end; hence thesis by A1,Def13;
end;

theorem
  f is convergent_in+infty implies (lim_in+infty f=g iff
for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1)
proof assume A1: f is convergent_in+infty;
thus lim_in+infty f=g implies
for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1
 proof assume A2: lim_in+infty f=g;
  given g1 such that
  A3: 0<g1 & for r ex r1 st r<r1 & r1 in dom f & abs(f.r1-g)>=g1;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f & abs(f.$2-g)>=g1;
  A4: now let n; consider r such that
  A5: n<r & r in dom f & abs(f.r-g)>=g1 by A3;
   reconsider r as real number;
   take r; thus X[n,r] by A5;
  end; consider s be Real_Sequence such that
  A6: for n holds X[n,s.n] from RealSeqChoice(A4);
 deffunc U(Nat) = $1;
  consider s1 be Real_Sequence such that
  A7: for n holds s1.n=U(n) from ExRealSeq;
  A8: s1 is divergent_to+infty by A7,Th47;
    now let n; n<s.n by A6; hence s1.n<=s.n by A7;end;
  then A9: s is divergent_to+infty by A8,Th69;
    now let x be set; assume x in rng s; then ex n st
 s.n=x by RFUNCT_2:9; hence x in dom f by A6;
  end; then A10: rng s c=dom f by TARSKI:def 3;
  then f*s is convergent & lim(f*s)=g by A1,A2,A9,Def12;
  then consider n such that A11: for m st n<=m holds abs((f*s).m-g)<g1 by A3,
SEQ_2:def 7;
    abs((f*s).n-g)<g1 by A11; then abs(f.(s.n)-g)<g1 by A10,RFUNCT_2:21;
  hence contradiction by A6;
 end;
 assume A12: for g1 st 0<g1 ex r st
 for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1;
   now let s be Real_Sequence such that
  A13: s is divergent_to+infty & rng s c=dom f;
  A14: now let g1 be real number;
A15:  g1 is Real by XREAL_0:def 1;
  assume 0<g1; then consider r such that
   A16: for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1 by A12,A15;
   consider n such that A17: for m st n<=m holds r<s.m by A13,Def4;
   take n; let m; assume n<=m; then A18: r<s.m by A17;
     s.m in rng s by RFUNCT_2:10;
   then abs(f.(s.m)-g)<g1 by A13,A16,A18;
   hence abs((f*s).m-g)<g1 by A13,RFUNCT_2:21;
  end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A14,SEQ_2:
def 7;
 end; hence thesis by A1,Def12;
end;

theorem Th115:
f is convergent_in+infty implies r(#)f is convergent_in+infty &
lim_in+infty(r(#)f)=r*(lim_in+infty f)
proof assume A1: f is convergent_in+infty;
 A2: for r1 ex g st r1<g & g in dom(r(#)f)
  proof let r1; consider g such that A3: r1<g & g in dom f by A1,Def6;
   take g; thus r1<g & g in dom(r(#)f) by A3,SEQ_1:def 6;
  end;
 A4: now let seq; A5: lim_in+infty f=lim_in+infty f;
  assume seq is divergent_to+infty & rng seq c=dom(r(#)f);
  then A6: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6;
  then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12;
  then r(#)(f*seq) is convergent by SEQ_2:21;
  hence (r(#)f)*seq is convergent by A6,RFUNCT_2:24;
  thus lim((r(#)f)*seq)=lim(r(#)(f*seq)) by A6,RFUNCT_2:24
  .=r*(lim_in+infty f) by A7,SEQ_2:22;
 end; hence r(#)f is convergent_in+infty by A2,Def6; hence thesis by A4,Def12
;
end;

theorem Th116:
f is convergent_in+infty implies -f is convergent_in+infty &
lim_in+infty(-f)=-(lim_in+infty f)
proof assume A1: f is convergent_in+infty; A2: (-1)(#)f=-f by RFUNCT_1:38;
 hence -f is convergent_in+infty by A1,Th115;
 thus lim_in+infty (-f)=(-1)*(lim_in+infty f) by A1,A2,Th115
 .=-(1*(lim_in+infty f)) by XCMPLX_1:175
 .=-(lim_in+infty f);
end;

theorem Th117:
f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1+f2)) implies f1+f2 is convergent_in+infty &
lim_in+infty(f1+f2) = lim_in+infty f1 + lim_in+infty f2
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 for r ex g st r<g & g in dom(f1+f2);
 A2: now let seq; A3: lim_in+infty f1=lim_in+infty f1 &
   lim_in+infty f2=lim_in+infty f2;
  assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2);
  then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by
Lm3;
  then A6: f1*seq is convergent & lim(f1*seq)=lim_in+infty f1 by A1,A3,A4,Def12
;
  A7: f2*seq is convergent & lim(f2*seq)=lim_in+infty f2
    by A1,A3,A4,A5,Def12;
  then f1*seq+f2*seq is convergent by A6,SEQ_2:19;
  hence (f1+f2)*seq is convergent by A4,A5,RFUNCT_2:23;
  thus lim((f1+f2)*seq)=lim(f1*seq+f2*seq) by A4,A5,RFUNCT_2:23
  .=lim_in+infty f1+lim_in+infty f2 by A6,A7,SEQ_2:20;
 end; hence f1+f2 is convergent_in+infty by A1,Def6; hence thesis by A2,Def12
;
end;

theorem
  f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1-f2)) implies f1-f2 is convergent_in+infty &
lim_in+infty(f1-f2)=(lim_in+infty f1)-(lim_in+infty f2)
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 for r ex g st r<g & g in dom(f1-f2);
 A2: now let r; consider g such that A3: r<g & g in dom(f1-f2) by A1;
  take g; thus r<g & g in dom(f1+-f2) by A3,RFUNCT_1:40;
 end;
 A4: -f2 is convergent_in+infty & lim_in+infty(-f2)=-(lim_in+infty f2)
   by A1,Th116;
 then f1+-f2 is convergent_in+infty by A1,A2,Th117;
 hence f1-f2 is convergent_in+infty by RFUNCT_1:40;
 thus lim_in+infty(f1-f2)=lim_in+infty(f1+-f2) by RFUNCT_1:40
 .=lim_in+infty f1+-lim_in+infty f2 by A1,A2,A4,Th117
 .=lim_in+infty f1-lim_in+infty f2 by XCMPLX_0:def 8;
end;

theorem
  f is convergent_in+infty & f"{0}={} & (lim_in+infty f)<>0 implies
f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)"
proof assume A1: f is convergent_in+infty & f"{0}={} & (lim_in+infty f)<>0;
 then A2: dom f= dom f\f"{0}
  .=dom(f^) by RFUNCT_1:def 8;
 then A3: for r ex g st r<g & g in dom(f^) by A1,Def6;
 A4: now let seq; assume A5: seq is divergent_to+infty & rng seq c=dom(f^);
  then A6: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A2,Def12;
  A7: f*seq is_not_0 by A5,RFUNCT_2:26;
  then (f*seq)" is convergent by A1,A6,SEQ_2:35;
  hence (f^)*seq is convergent by A5,RFUNCT_2:27;
  thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27
  .=(lim_in+infty f)" by A1,A6,A7,SEQ_2:36;
 end; hence f^ is convergent_in+infty by A3,Def6; hence thesis by A4,Def12;
end;

theorem
  f is convergent_in+infty implies abs(f) is convergent_in+infty &
lim_in+infty abs(f)=abs(lim_in+infty f)
proof assume A1: f is convergent_in+infty;
 A2: now let r; consider g such that A3: r<g & g in dom f by A1,Def6;
  take g; thus r<g & g in dom abs(f) by A3,SEQ_1:def 10;
 end;
 A4: now let seq; A5: lim_in+infty f=lim_in+infty f;
  assume seq is divergent_to+infty & rng seq c=dom abs(f);
  then A6: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 10;
  then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12;
  then abs(f*seq) is convergent by SEQ_4:26;
  hence abs(f)*seq is convergent by A6,RFUNCT_2:25;
  thus lim(abs(f)*seq)=lim abs(f*seq) by A6,RFUNCT_2:25
  .=abs(lim_in+infty f) by A7,SEQ_4:27;
 end; hence abs(f) is convergent_in+infty by A2,Def6; hence thesis by A4,Def12;
end;

theorem Th121:
f is convergent_in+infty & lim_in+infty f<>0 &
(for r ex g st r<g & g in dom f & f.g<>0) implies
f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)"
proof assume A1: f is convergent_in+infty & lim_in+infty f<>0 &
 for r ex g st r<g & g in dom f & f.g<>0;
 A2: now let r; consider g such that A3: r<g & g in dom f & f.g<>0 by A1;
  take g; not f.g in {0} by A3,TARSKI:def 1;
  then not g in f"{0} by FUNCT_1:def 13;
  then g in dom f\f"{0} by A3,XBOOLE_0:def 4;
  hence r<g & g in dom(f^) by A3,RFUNCT_1:def 8;
 end;
 A4: now let seq such that A5: seq is divergent_to+infty & rng seq c=dom(f^);
  A6: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8
; dom f\f"{0}c=dom f by XBOOLE_1:36;
  then rng seq c=dom f by A5,A6,XBOOLE_1:1;
  then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12;
  A8: f*seq is_not_0 by A5,RFUNCT_2:26;
  then (f*seq)" is convergent by A1,A7,SEQ_2:35;
  hence (f^)*seq is convergent by A5,RFUNCT_2:27;
  thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27
  .=(lim_in+infty f)" by A1,A7,A8,SEQ_2:36;
 end; hence f^ is convergent_in+infty by A2,Def6; hence thesis by A4,Def12;
end;

theorem Th122:
f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1(#)f2)) implies f1(#)
f2 is convergent_in+infty &
lim_in+infty(f1(#)f2)=(lim_in+infty f1)*(lim_in+infty f2)
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 for r ex g st r<g & g in dom(f1(#)f2);
 A2: now let seq; A3: lim_in+infty f1=lim_in+infty f1 &
   lim_in+infty f2=lim_in+infty f2;
  assume A4: seq is divergent_to+infty & rng seq c=dom(f1(#)f2);
  then A5: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2
by Lm4;
  then A6: f1*seq is convergent & lim(f1*seq)=lim_in+infty f1 by A1,A3,A4,Def12
;
  A7: f2*seq is convergent & lim(f2*seq)=lim_in+infty f2 by A1,A3,A4,A5,Def12;
  then (f1*seq)(#)(f2*seq) is convergent by A6,SEQ_2:28;
  hence (f1(#)f2)*seq is convergent by A4,A5,RFUNCT_2:23;
  thus lim((f1(#)f2)*seq)=lim((f1*seq)(#)(f2*seq)) by A4,A5,RFUNCT_2:23
  .=(lim_in+infty f1)*(lim_in+infty f2) by A6,A7,SEQ_2:29;
 end; hence f1(#)
f2 is convergent_in+infty by A1,Def6; hence thesis by A2,Def12;
end;

theorem
  f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2<>0 &
(for r ex g st r<g & g in dom(f1/f2)) implies f1/f2 is convergent_in+infty &
lim_in+infty(f1/f2)=(lim_in+infty f1)/(lim_in+infty f2)
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 lim_in+infty f2<>0 & for r ex g st r<g & g in dom(f1/f2);
    dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4;
  then A2: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 8;
  A3: dom f1/\dom(f2^)c=dom f1 & dom f1/\dom(f2^)c=dom(f2^) by XBOOLE_1:17;
 A4: now let r; consider g such that A5: r<g & g in dom(f1/f2) by A1;
  take g; thus r<g & g in dom(f1(#)(f2^)) by A2,A5,SEQ_1:def 5;
 end;
   now let r; consider g such that A6: r<g & g in dom(f1/f2) by A1;
  take g; g in dom(f2^) by A2,A3,A6;
  then A7: g in dom f2\f2"{0} by RFUNCT_1:def 8;
  then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 4;
  then not f2.g in {0} by FUNCT_1:def 13;
  hence r<g & g in dom f2 & f2.g<>0 by A6,A7,TARSKI:def 1,XBOOLE_0:def 4;
 end;
 then A8: f2^ is convergent_in+infty & lim_in+infty(f2^)=(lim_in+infty f2)"
   by A1,Th121;
 then f1(#)(f2^) is convergent_in+infty by A1,A4,Th122;
 hence f1/f2 is convergent_in+infty by RFUNCT_1:47;
 thus lim_in+infty(f1/f2)=lim_in+infty(f1(#)(f2^)) by RFUNCT_1:47
 .=(lim_in+infty f1)*((lim_in+infty f2)") by A1,A4,A8,Th122
 .=(lim_in+infty f1)/(lim_in+infty f2) by XCMPLX_0:def 9;
end;

theorem Th124:
f is convergent_in-infty implies r(#)f is convergent_in-infty &
lim_in-infty(r(#)f)=r*(lim_in-infty f)
proof assume A1: f is convergent_in-infty;
 A2: for r1 ex g st g<r1 & g in dom(r(#)f)
  proof let r1; consider g such that A3: g<r1 & g in dom f by A1,Def9;
   take g; thus g<r1 & g in dom(r(#)f) by A3,SEQ_1:def 6;
  end;
 A4: now let seq; A5: lim_in-infty f=lim_in-infty f;
  assume seq is divergent_to-infty & rng seq c=dom(r(#)f);
  then A6: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6;
  then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13;
  then r(#)(f*seq) is convergent by SEQ_2:21;
  hence (r(#)f)*seq is convergent by A6,RFUNCT_2:24;
  thus lim((r(#)f)*seq)=lim(r(#)(f*seq)) by A6,RFUNCT_2:24
  .=r*(lim_in-infty f) by A7,SEQ_2:22;
 end; hence r(#)f is convergent_in-infty by A2,Def9; hence thesis by A4,Def13
;
end;

theorem Th125:
f is convergent_in-infty implies -f is convergent_in-infty &
lim_in-infty(-f)=-(lim_in-infty f)
proof assume A1: f is convergent_in-infty; A2: (-1)(#)f=-f by RFUNCT_1:38;
 hence -f is convergent_in-infty by A1,Th124;
 thus lim_in-infty (-f)=(-1)*(lim_in-infty f) by A1,A2,Th124
 .=-(1*(lim_in-infty f)) by XCMPLX_1:175
 .=-(lim_in-infty f);
end;

theorem Th126:
f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1+f2)) implies f1+f2 is convergent_in-infty &
lim_in-infty(f1+f2) = lim_in-infty f1 + lim_in-infty f2
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 for r ex g st g<r & g in dom(f1+f2);
 A2: now let seq; A3: lim_in-infty f1=lim_in-infty f1 &
   lim_in-infty f2=lim_in-infty f2;
  assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2);
  then A5: rng seq c=dom f1/\dom f2 by SEQ_1:def 3;
    dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  then A6: rng seq c=dom f1 & rng seq c=dom f2 by A5,XBOOLE_1:1;
  then A7: f1*seq is convergent & lim(f1*seq)=lim_in-infty f1 by A1,A3,A4,Def13
;
  A8: f2*seq is convergent & lim(f2*seq)=lim_in-infty f2 by A1,A3,A4,A6,Def13;
  then f1*seq+f2*seq is convergent by A7,SEQ_2:19;
  hence (f1+f2)*seq is convergent by A5,RFUNCT_2:23;
  thus lim((f1+f2)*seq)=lim(f1*seq+f2*seq) by A5,RFUNCT_2:23
  .=lim_in-infty f1+lim_in-infty f2 by A7,A8,SEQ_2:20;
 end; hence f1+f2 is convergent_in-infty by A1,Def9; hence thesis by A2,Def13
;
end;

theorem
  f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1-f2)) implies f1-f2 is convergent_in-infty &
lim_in-infty(f1-f2)=(lim_in-infty f1)-(lim_in-infty f2)
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 for r ex g st g<r & g in dom(f1-f2);
 A2: now let r; consider g such that A3: g<r & g in dom(f1-f2) by A1;
  take g; thus g<r & g in dom(f1+-f2) by A3,RFUNCT_1:40;
 end;
 A4: -f2 is convergent_in-infty & lim_in-infty(-f2)=-(lim_in-infty f2)
   by A1,Th125;
 then f1+-f2 is convergent_in-infty by A1,A2,Th126;
 hence f1-f2 is convergent_in-infty by RFUNCT_1:40;
 thus lim_in-infty(f1-f2)=lim_in-infty(f1+-f2) by RFUNCT_1:40
 .=lim_in-infty f1+-lim_in-infty f2 by A1,A2,A4,Th126
 .=lim_in-infty f1-lim_in-infty f2 by XCMPLX_0:def 8;
end;

theorem
  f is convergent_in-infty & f"{0}={} & (lim_in-infty f)<>0 implies
f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)"
proof assume A1: f is convergent_in-infty & f"{0}={} & (lim_in-infty f)<>0;
 then A2: dom f= dom f\f"{0}
  .=dom(f^) by RFUNCT_1:def 8;
 then A3: for r ex g st g<r & g in dom(f^) by A1,Def9;
 A4: now let seq; assume A5: seq is divergent_to-infty & rng seq c=dom(f^);
  then A6: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A2,Def13;
  A7: f*seq is_not_0 by A5,RFUNCT_2:26;
  then (f*seq)" is convergent by A1,A6,SEQ_2:35;
  hence (f^)*seq is convergent by A5,RFUNCT_2:27;
  thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27
  .=(lim_in-infty f)" by A1,A6,A7,SEQ_2:36;
 end; hence f^ is convergent_in-infty by A3,Def9; hence thesis by A4,Def13;
end;

theorem
  f is convergent_in-infty implies abs(f) is convergent_in-infty &
lim_in-infty abs(f)=abs(lim_in-infty f)
proof assume A1: f is convergent_in-infty;
 A2: now let r; consider g such that A3: g<r & g in dom f by A1,Def9;
  take g; thus g<r & g in dom abs(f) by A3,SEQ_1:def 10;
 end;
 A4: now let seq; A5: lim_in-infty f=lim_in-infty f;
  assume seq is divergent_to-infty & rng seq c=dom abs(f);
  then A6: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 10;
  then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13;
  then abs(f*seq) is convergent by SEQ_4:26;
  hence abs(f)*seq is convergent by A6,RFUNCT_2:25;
  thus lim(abs(f)*seq)=lim abs(f*seq) by A6,RFUNCT_2:25
  .=abs(lim_in-infty f) by A7,SEQ_4:27;
 end; hence abs(f) is convergent_in-infty by A2,Def9; hence thesis by A4,Def13;
end;

theorem Th130:
f is convergent_in-infty & lim_in-infty f<>0 &
(for r ex g st g<r & g in dom f & f.g<>0) implies
f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)"
proof assume A1: f is convergent_in-infty & lim_in-infty f<>0 &
 for r ex g st g<r & g in dom f & f.g<>0;
 A2: now let r; consider g such that A3: g<r & g in dom f & f.g<>0 by A1;
  take g; not f.g in {0} by A3,TARSKI:def 1;
  then not g in f"{0} by FUNCT_1:def 13;
  then g in dom f\f"{0} by A3,XBOOLE_0:def 4;
  hence g<r & g in dom(f^) by A3,RFUNCT_1:def 8;
 end;
 A4: now let seq such that A5: seq is divergent_to-infty & rng seq c=dom(f^);
  A6: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8
; dom f\f"{0}c=dom f by XBOOLE_1:36;
  then rng seq c=dom f by A5,A6,XBOOLE_1:1;
  then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13;
  A8: f*seq is_not_0 by A5,RFUNCT_2:26;
  then (f*seq)" is convergent by A1,A7,SEQ_2:35;
  hence (f^)*seq is convergent by A5,RFUNCT_2:27;
  thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27
  .=(lim_in-infty f)" by A1,A7,A8,SEQ_2:36;
 end; hence f^ is convergent_in-infty by A2,Def9; hence thesis by A4,Def13;
end;

theorem Th131:
f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1(#)f2)) implies f1(#)
f2 is convergent_in-infty &
lim_in-infty(f1(#)f2)=(lim_in-infty f1)*(lim_in-infty f2)
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 for r ex g st g<r & g in dom(f1(#)f2);
 A2: now let seq; A3: lim_in-infty f1=lim_in-infty f1 &
   lim_in-infty f2=lim_in-infty f2;
  assume A4: seq is divergent_to-infty & rng seq c=dom(f1(#)f2);
  A5: dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  A6: dom(f1(#)f2)=dom f1/\dom f2 by SEQ_1:def 5;
  then rng seq c=dom f1 by A4,A5,XBOOLE_1:1;
  then A7: f1*seq is convergent & lim(f1*seq)=lim_in-infty f1 by A1,A3,A4,Def13
;
    rng seq c=dom f2 by A4,A5,A6,XBOOLE_1:1;
  then A8: f2*seq is convergent & lim(f2*seq)=lim_in-infty f2 by A1,A3,A4,Def13
;
  then (f1*seq)(#)(f2*seq) is convergent by A7,SEQ_2:28;
  hence (f1(#)f2)*seq is convergent by A4,A6,RFUNCT_2:23;
  thus lim((f1(#)f2)*seq)=lim((f1*seq)(#)(f2*seq)) by A4,A6,RFUNCT_2:23
  .=(lim_in-infty f1)*(lim_in-infty f2) by A7,A8,SEQ_2:29;
 end; hence f1(#)
f2 is convergent_in-infty by A1,Def9; hence thesis by A2,Def13;
end;

theorem
  f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2<>0 &
(for r ex g st g<r & g in dom(f1/f2)) implies f1/f2 is convergent_in-infty &
lim_in-infty(f1/f2)=(lim_in-infty f1)/(lim_in-infty f2)
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 lim_in-infty f2<>0 & for r ex g st g<r & g in dom(f1/f2);
    dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4;
  then A2: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 8;
  A3: dom f1/\dom(f2^) c=dom f1 & dom f1/\dom(f2^) c=dom(f2^) by XBOOLE_1:17;
 A4: now let r; consider g such that A5: g<r & g in dom(f1/f2) by A1;
  take g; thus g<r & g in dom(f1(#)(f2^)) by A2,A5,SEQ_1:def 5;
 end;
   now let r; consider g such that A6: g<r & g in dom(f1/f2) by A1;
  take g; g in dom(f2^) by A2,A3,A6;
  then A7: g in dom f2\f2"{0} by RFUNCT_1:def 8;
  then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 4;
  then not f2.g in {0} by FUNCT_1:def 13;
  hence g<r & g in dom f2 & f2.g<>0 by A6,A7,TARSKI:def 1,XBOOLE_0:def 4;
 end;
 then A8: f2^ is convergent_in-infty & lim_in-infty(f2^)=(lim_in-infty f2)"
   by A1,Th130;
 then f1(#)(f2^) is convergent_in-infty by A1,A4,Th131;
 hence f1/f2 is convergent_in-infty by RFUNCT_1:47;
 thus lim_in-infty(f1/f2)=lim_in-infty(f1(#)(f2^)) by RFUNCT_1:47
 .=(lim_in-infty f1)*((lim_in-infty f2)") by A1,A4,A8,Th131
 .=(lim_in-infty f1)/(lim_in-infty f2) by XCMPLX_0:def 9;
end;

theorem
  f1 is convergent_in+infty & lim_in+infty f1=0 &
(for r ex g st r<g & g in dom(f1(#)f2)) &
(ex r st f2 is_bounded_on right_open_halfline(r)) implies
f1(#)f2 is convergent_in+infty & lim_in+infty(f1(#)f2)=0
proof assume A1: f1 is convergent_in+infty & lim_in+infty f1=0 &
 for r ex g st r<g & g in dom(f1(#)f2);
 given r such that A2: f2 is_bounded_on right_open_halfline(r);
 consider g be real number such that
 A3: for r1 st r1 in right_open_halfline(r)/\dom f2 holds
  abs(f2.r1)<=g by A2,RFUNCT_1:90;
 A4: now let s be Real_Sequence; assume
  A5: s is divergent_to+infty & rng s c=dom(f1(#)f2);
  then A6: dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 by Lm4
;
  consider k such that A7: for n st k<=n holds r<s.n by A5,Def4;
    s^\k is_subsequence_of s by SEQM_3:47;
  then A8: s^\k is divergent_to+infty by A5,Th53; rng(s^\k)c=rng s
    by RFUNCT_2:7;
  then A9: rng(s^\k)c=dom f1/\dom f2 & rng(s^\k)c=dom f1 & rng(s^\k)c=dom f2
   by A5,A6,XBOOLE_1:1;
  then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def12;
    now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm2;
   let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37;
then r<s.(n+k) by A7;
   then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g1: r<g1};
   then (s^\k).n in right_open_halfline(r) by Def3;
   then (s^\k).n in right_open_halfline(r)/\dom f2 by A9,A11,XBOOLE_0:def 3;
   then abs(f2.((s^\k).n))<=g by A3; then A12: abs((f2*(s^\k)).n)<=
g by A9,RFUNCT_2:21;
     g<=abs(g) by ABSVALUE:11; then g<t by Lm2;
   hence abs((f2*(s^\k)).n)<t by A12,AXIOMS:22;
  end; then A13: f2*(s^\k) is bounded by SEQ_2:15;
  then A14: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39;
  A15: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A13,SEQ_2:40;
  A16: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23
  .=((f1(#)f2)*s)^\k by A5,RFUNCT_2:22;
  hence (f1(#)f2)*s is convergent by A14,SEQ_4:35;
  thus lim((f1(#)f2)*s)=0 by A14,A15,A16,SEQ_4:36;
 end; hence f1(#)
f2 is convergent_in+infty by A1,Def6; hence thesis by A4,Def12;
end;

theorem
  f1 is convergent_in-infty & lim_in-infty f1=0 &
(for r ex g st g<r & g in dom(f1(#)f2)) &
(ex r st f2 is_bounded_on left_open_halfline(r)) implies
f1(#)f2 is convergent_in-infty & lim_in-infty(f1(#)f2)=0
proof assume A1: f1 is convergent_in-infty & lim_in-infty f1=0 &
 for r ex g st g<r & g in dom(f1(#)f2);
 given r such that A2: f2 is_bounded_on left_open_halfline(r);
 consider g be real number such that
 A3: for r1 st r1 in left_open_halfline(r)/\dom f2 holds
  abs(f2.r1)<=g by A2,RFUNCT_1:90;
 A4: now let s be Real_Sequence; assume
  A5: s is divergent_to-infty & rng s c=dom(f1(#)f2);
  then A6: dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 by Lm4
;
  consider k such that A7: for n st k<=n holds s.n<r by A5,Def5;
    s^\k is_subsequence_of s by SEQM_3:47;
  then A8: s^\k is divergent_to-infty by A5,Th54;
    rng(s^\k)c=rng s by RFUNCT_2:7;
  then A9: rng(s^\k)c=dom f1/\dom f2 & rng(s^\k)c=dom f1 & rng(s^\k)c=dom f2
   by A5,A6,XBOOLE_1:1;
  then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def13;
    now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm2;
   let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37;
then s.(n+k)<r by A7;
   then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g1: g1<r};
   then (s^\k).n in left_open_halfline(r) by PROB_1:def 15;
   then (s^\k).n in left_open_halfline(r)/\dom f2 by A9,A11,XBOOLE_0:def 3;
   then abs(f2.((s^\k).n))<=g by A3; then A12: abs((f2*(s^\k)).n)<=
g by A9,RFUNCT_2:21;
     g<=abs(g) by ABSVALUE:11; then g<t by Lm2;
   hence abs((f2*(s^\k)).n)<t by A12,AXIOMS:22;
  end; then A13: f2*(s^\k) is bounded by SEQ_2:15;
  then A14: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39;
  A15: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A13,SEQ_2:40;
  A16: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23
  .=((f1(#)f2)*s)^\k by A5,RFUNCT_2:22;
  hence (f1(#)f2)*s is convergent by A14,SEQ_4:35;
  thus lim((f1(#)f2)*s)=0 by A14,A15,A16,SEQ_4:36;
 end; hence f1(#)
f2 is convergent_in-infty by A1,Def9; hence thesis by A4,Def13;
end;

theorem Th135:
f1 is convergent_in+infty & f2 is convergent_in+infty &
lim_in+infty f1=lim_in+infty f2 & (for r ex g st r<g & g in dom f) & (ex r st
 ((dom f1 /\ right_open_halfline(r) c= dom f2 /\ right_open_halfline(r) &
   dom f /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r)) or
  (dom f2 /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
   dom f /\ right_open_halfline(r) c= dom f2 /\ right_open_halfline(r))) &
 for g st g in dom f /\ right_open_halfline(r) holds
  f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in+infty & lim_in+infty f=lim_in+infty f1
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 lim_in+infty f1=lim_in+infty f2 & (for r ex g st r<g & g in dom f);
 given r1 such that
 A2: (dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) &
  dom f/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1)) or
   (dom f2/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1) &
   dom f/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1)) and
 A3: for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
   now per cases by A2;
 suppose A4: dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) &
  dom f/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1);
  A5: now let seq; assume A6: seq is divergent_to+infty & rng seq c=dom f;
   then consider k such that A7: for n st k<=n holds r1<seq.n by Def4;
     seq^\k is_subsequence_of seq by SEQM_3:47;
   then A8: seq^\k is divergent_to+infty by A6,Th53;
     now let x be set; assume x in rng(seq^\k); then consider n such that
    A9: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then r1<seq.(n+k) by A7;
    then r1<(seq^\k).n by SEQM_3:def 9; then x in {g: r1<g} by A9;
    hence x in right_open_halfline(r1) by Def3;
   end; then A10: rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3;
     rng(seq^\k)c=rng seq by RFUNCT_2:7;
   then A11: rng(seq^\k)c=dom f by A6,XBOOLE_1:1;
   then A12: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A10,XBOOLE_1:19;
   then A13: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A4,XBOOLE_1:1;
     dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
   then A14: rng(seq^\k)c=dom f1 by A13,XBOOLE_1:1;
   then A15: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in+infty f1
     by A1,A8,Def12;
   A16: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A4,A13,XBOOLE_1:1;
     dom f2/\right_open_halfline(r1) c=dom f2 by XBOOLE_1:17;
   then A17: rng(seq^\k)c=dom f2 by A16,XBOOLE_1:1;
   then A18: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in+infty f1
     by A1,A8,Def12;
   A19: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
    then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by
A3,A12
;
    then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
     by A11,RFUNCT_2:21;
    hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
     by A14,A17,RFUNCT_2:21;
   end; A20: f*(seq^\k)=(f*seq)^\k by A6,RFUNCT_2:22;
   then (f*seq)^\k is convergent by A15,A18,A19,SEQ_2:33;
   hence A21: f*seq is convergent by SEQ_4:35;
     lim((f*seq)^\k)=lim_in+infty f1 by A15,A18,A19,A20,SEQ_2:34;
   hence lim(f*seq)=lim_in+infty f1 by A21,SEQ_4:33;
  end; hence f is convergent_in+infty by A1,Def6; hence thesis by A5,Def12;
 suppose A22: dom f2/\right_open_halfline(r1)c=dom f1/\
right_open_halfline(r1) &
  dom f/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1);
  A23: now let seq; assume A24: seq is divergent_to+infty & rng seq c=dom f;
   then consider k such that A25: for n st k<=n holds r1<seq.n by Def4;
     seq^\k is_subsequence_of seq by SEQM_3:47;
   then A26: seq^\k is divergent_to+infty by A24,Th53;
     now let x be set; assume x in rng(seq^\k); then consider n such that
    A27: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then r1<seq.(n+k) by A25;
    then r1<(seq^\k).n by SEQM_3:def 9; then x in {g: r1<g} by A27;
    hence x in right_open_halfline(r1) by Def3;
   end; then A28: rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3;
     rng(seq^\k) c=rng seq by RFUNCT_2:7;
   then A29: rng(seq^\k)c=dom f by A24,XBOOLE_1:1;
   then A30: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A28,XBOOLE_1:19;
   then A31: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A22,XBOOLE_1:1;
     dom f2/\right_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
   then A32: rng(seq^\k)c=dom f2 by A31,XBOOLE_1:1;
   then A33: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in+infty f1
     by A1,A26,Def12;
   A34: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A22,A31,XBOOLE_1:1;
     dom f1/\right_open_halfline(r1) c=dom f1 by XBOOLE_1:17;
   then A35: rng(seq^\k)c=dom f1 by A34,XBOOLE_1:1;
   then A36: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in+infty f1
     by A1,A26,Def12;
   A37: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
    then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by
A3,A30
;
    then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
     by A29,RFUNCT_2:21;
    hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
     by A32,A35,RFUNCT_2:21;
   end; A38: f*(seq^\k)=(f*seq)^\k by A24,RFUNCT_2:22;
   then (f*seq)^\k is convergent by A33,A36,A37,SEQ_2:33;
   hence A39: f*seq is convergent by SEQ_4:35;
     lim((f*seq)^\k)=lim_in+infty f1 by A33,A36,A37,A38,SEQ_2:34;
   hence lim(f*seq)=lim_in+infty f1 by A39,SEQ_4:33;
  end; hence f is convergent_in+infty by A1,Def6; hence thesis by A23,Def12;
 end; hence thesis;
end;

theorem
  f1 is convergent_in+infty & f2 is convergent_in+infty &
  lim_in+infty f1=lim_in+infty f2
& (ex r st right_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f &
for g st g in right_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in+infty & lim_in+infty f=lim_in+infty f1
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty &
 lim_in+infty f1=lim_in+infty f2;
 given r1 such that A2: right_open_halfline(r1)c=dom f1/\dom f2/\dom f &
  for g st g in right_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
 A3: dom f1/\dom f2/\dom f c=dom f & dom f1/\dom f2/\dom f c=dom f1/\dom f2
  by XBOOLE_1:17;
 then A4: right_open_halfline(r1)c=dom f by A2,XBOOLE_1:1;
 A5: now let r; consider g being real number such that
 A6: abs(r)+abs(r1)<g by REAL_1:76;
  reconsider g as Real by XREAL_0:def 1;
  take g; A7: r<=abs(r) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
  then r+0<=abs(r)+abs(r1) by A7,REAL_1:55;
  hence r<g by A6,AXIOMS:22;
  A8: r1<=abs(r1) by ABSVALUE:11; 0<=abs(r) by ABSVALUE:5;
  then 0+r1<=abs(r)+abs(r1) by A8,REAL_1:55;
  then r1<g by A6,AXIOMS:22; then g in {g1: r1<g1};
  then g in right_open_halfline(r1) by Def3; hence g in dom f by A4;
 end;
   now dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  then dom f1/\dom f2/\dom f c=dom f1 & dom f1/\dom f2/\
dom f c=dom f2 by A3,XBOOLE_1:1;
  then A9: right_open_halfline(r1)c=dom f1 & right_open_halfline(r1)c=dom f2
   by A2,XBOOLE_1:1;
  then A10: dom f1/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1
:28;
  hence dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) by A9,
XBOOLE_1:28;
  thus dom f/\right_open_halfline(r1)c=dom f1/\
right_open_halfline(r1) by A4,A10,XBOOLE_1:28;
  let g; assume g in dom f/\right_open_halfline(r1);
  then g in right_open_halfline(r1) by XBOOLE_0:def 3;
  hence f1.g<=f.g & f.g<=f2.g by A2;
 end; hence thesis by A1,A5,Th135;
end;

theorem Th137:
f1 is convergent_in-infty & f2 is convergent_in-infty &
lim_in-infty f1=lim_in-infty f2 & (for r ex g st g<r & g in dom f) & (ex r st
 ((dom f1 /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r) &
   dom f /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r)) or
  (dom f2 /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
   dom f /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r))) &
 for g st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g)
 implies
f is convergent_in-infty & lim_in-infty f=lim_in-infty f1
proof assume
A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 lim_in-infty f1=lim_in-infty f2 & (for r ex g st g<r & g in dom f);
 given r1 such that
 A2: (dom f1/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1) &
  dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1)) or
  (dom f2/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) &
   dom f/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1)) and
 A3: for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
   now per cases by A2;
 suppose A4: dom f1/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1) &
  dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1);
  A5: now let seq; assume A6: seq is divergent_to-infty & rng seq c=dom f;
   then consider k such that A7: for n st k<=n holds seq.n<r1 by Def5;
     seq^\k is_subsequence_of seq by SEQM_3:47;
   then A8: seq^\k is divergent_to-infty by A6,Th54;
     now let x be set; assume x in rng(seq^\k); then consider n such that
    A9: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then seq.(n+k)<r1 by A7;
    then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g: g<r1} by A9;
    hence x in left_open_halfline(r1) by PROB_1:def 15;
   end; then A10: rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3;
     rng(seq^\k)c=rng seq by RFUNCT_2:7;
   then A11: rng(seq^\k)c=dom f by A6,XBOOLE_1:1;
   then A12: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A10,XBOOLE_1:19;
   then A13: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A4,XBOOLE_1:1;
     dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
   then A14: rng(seq^\k)c=dom f1 by A13,XBOOLE_1:1;
   then A15: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in-infty f1
     by A1,A8,Def13;
   A16: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A4,A13,XBOOLE_1:1;
     dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
   then A17: rng(seq^\k)c=dom f2 by A16,XBOOLE_1:1;
   then A18: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in-infty f1
     by A1,A8,Def13;
   A19: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
    then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by
A3,A12
;
    then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
     by A11,RFUNCT_2:21;
    hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
     by A14,A17,RFUNCT_2:21;
   end; A20: f*(seq^\k)=(f*seq)^\k by A6,RFUNCT_2:22;
   then (f*seq)^\k is convergent by A15,A18,A19,SEQ_2:33;
   hence A21: f*seq is convergent by SEQ_4:35;
     lim((f*seq)^\k)=lim_in-infty f1 by A15,A18,A19,A20,SEQ_2:34;
   hence lim(f*seq)=lim_in-infty f1 by A21,SEQ_4:33;
  end; hence f is convergent_in-infty by A1,Def9; hence thesis by A5,Def13;
 suppose A22: dom f2/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) &
  dom f/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1);
  A23: now let seq; assume A24: seq is divergent_to-infty & rng seq c=dom f;
   then consider k such that A25: for n st k<=n holds seq.n<r1 by Def5;
     seq^\k is_subsequence_of seq by SEQM_3:47;
   then A26: seq^\k is divergent_to-infty by A24,Th54;
     now let x be set; assume x in rng(seq^\k); then consider n such that
    A27: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then seq.(n+k)<r1 by A25;
    then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g: g<r1} by A27;
    hence x in left_open_halfline(r1) by PROB_1:def 15;
   end; then A28: rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3;
     rng(seq^\k)c=rng seq by RFUNCT_2:7;
   then A29: rng(seq^\k)c=dom f by A24,XBOOLE_1:1;
   then A30: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A28,XBOOLE_1:19;
   then A31: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A22,XBOOLE_1:1;
     dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
   then A32: rng(seq^\k)c=dom f2 by A31,XBOOLE_1:1;
   then A33: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in-infty f1
     by A1,A26,Def13;
   A34: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A22,A31,XBOOLE_1:1;
     dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
   then A35: rng(seq^\k)c=dom f1 by A34,XBOOLE_1:1;
   then A36: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in-infty f1
     by A1,A26,Def13;
   A37: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
    then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by
A3,A30
;
    then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
     by A29,RFUNCT_2:21;
    hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
     by A32,A35,RFUNCT_2:21;
   end; A38: f*(seq^\k)=(f*seq)^\k by A24,RFUNCT_2:22;
   then (f*seq)^\k is convergent by A33,A36,A37,SEQ_2:33;
   hence A39: f*seq is convergent by SEQ_4:35;
     lim((f*seq)^\k)=lim_in-infty f1 by A33,A36,A37,A38,SEQ_2:34;
   hence lim(f*seq)=lim_in-infty f1 by A39,SEQ_4:33;
  end; hence f is convergent_in-infty by A1,Def9; hence thesis by A23,Def13;
 end; hence thesis;
end;

theorem
  f1 is convergent_in-infty & f2 is convergent_in-infty &
 lim_in-infty f1=lim_in-infty f2
& (ex r st left_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f &
for g st g in left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in-infty & lim_in-infty f=lim_in-infty f1
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty &
 lim_in-infty f1=lim_in-infty f2;
 given r1 such that A2: left_open_halfline(r1)c=dom f1/\dom f2/\dom f &
  for g st g in left_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
 A3: dom f1/\dom f2/\dom f c=dom f & dom f1/\dom f2/\dom f c=dom f1/\dom f2
  by XBOOLE_1:17;
 then A4: left_open_halfline(r1) c=dom f by A2,XBOOLE_1:1;
 A5: now let r; consider g being real number such that
 A6: g<-abs(r)-abs(r1) by REAL_1:77;
  reconsider g as Real by XREAL_0:def 1;
  take g; A7: -abs(r)<=r by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5;
  then -abs(r)-abs(r1)<=r-0 by A7,REAL_1:92; hence g<r by A6,AXIOMS:22;
  A8: -abs(r1)<=r1 by ABSVALUE:11; 0<=abs(r) by ABSVALUE:5;
  then -abs(r1)-abs(r)<=r1-0 by A8,REAL_1:92;
then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8;
  then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A6,AXIOMS:22;
  then g in {g1: g1<r1}; then g in left_open_halfline(r1) by PROB_1:def 15;
  hence g in dom f by A4;
 end;
   now dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
  then dom f1/\dom f2/\dom f c=dom f1 & dom f1/\dom f2/\
dom f c=dom f2 by A3,XBOOLE_1:1;
  then A9: left_open_halfline(r1)c=dom f1 & left_open_halfline(r1)c=dom f2
   by A2,XBOOLE_1:1;
  then A10: dom f1/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1:
28;
  hence dom f1/\left_open_halfline(r1) c=dom f2/\left_open_halfline(r1) by A9,
XBOOLE_1:28;
  thus dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) by A4,A10,
XBOOLE_1:28;
  let g; assume g in dom f/\left_open_halfline(r1);
  then g in left_open_halfline(r1) by XBOOLE_0:def 3;
  hence f1.g<=f.g & f.g<=f2.g by A2;
 end; hence thesis by A1,A5,Th137;
end;

theorem
  f1 is convergent_in+infty & f2 is convergent_in+infty &
(ex r st ((dom f1 /\ right_open_halfline(r) c= dom f2 /\
 right_open_halfline(r) &
 for g st g in dom f1 /\ right_open_halfline(r) holds f1.g<=f2.g) or
 (dom f2 /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
 for g st g in dom f2 /\ right_open_halfline(r) holds f1.g<=f2.g))) implies
lim_in+infty f1<=lim_in+infty f2
proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty;
 given r such that
 A2: (dom f1/\right_open_halfline(r)c=dom f2/\right_open_halfline(r) &
 for g st g in dom f1/\right_open_halfline(r) holds f1.g<=f2.g) or
 (dom f2/\right_open_halfline(r)c=dom f1/\right_open_halfline(r) &
 for g st g in dom f2/\right_open_halfline(r) holds f1.g<=f2.g);
   now per cases by A2;
 suppose A3: dom f1/\right_open_halfline(r)c=dom f2/\right_open_halfline(r) &
  for g st g in dom f1/\right_open_halfline(r) holds f1.g<=f2.g;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f1/\right_open_halfline r;
  A4: now let n; consider g such that A5: n+abs(r)<g & g in dom f1 by A1,Def6;
   reconsider g as real number;
   take g; 0<=abs(r) by ABSVALUE:5; then
A6:  n+0<=n+abs(r) by REAL_1:55;
   A7: 0<=n by NAT_1:18; r<=abs(r) by ABSVALUE:11;
   then 0+r<=n+abs(r) by A7,REAL_1:55;
   then r<g by A5,AXIOMS:22; then g in {g2: r<g2};
   then g in right_open_halfline(r) by Def3;
   hence X[n,g] by A5,A6,AXIOMS:22,XBOOLE_0:def 3;
  end; consider s1 be Real_Sequence such that
  A8: for n holds X[n,s1.n] from RealSeqChoice(A4);
 deffunc U(Nat) = $1;
  consider s2 be Real_Sequence such that
  A9: for n holds s2.n=U(n) from ExRealSeq;
  A10: s2 is divergent_to+infty by A9,Th47;
    now let n; n<s1.n by A8; hence s2.n<=s1.n by A9;
  end; then A11: s1 is divergent_to+infty by A10,Th69;
  A12: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2;
  A13: rng s1 c=dom f1
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f1/\right_open_halfline(r) by A8;
   hence x in dom f1 by XBOOLE_0:def 3;
  end; then A14: f1*s1 is convergent & lim(f1*s1)=lim_in+infty f1
    by A1,A11,A12,Def12;
  A15: rng s1 c=dom f2
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f1/\right_open_halfline(r) by A8;
hence x in dom f2 by A3,XBOOLE_0:def 3;
  end; then A16: f2*s1 is convergent & lim(f2*s1)=lim_in+infty f2
    by A1,A11,A12,Def12;
    now let n; s1.n in dom f1/\right_open_halfline(r) by A8;
   then f1.(s1.n)<=f2.(s1.n) by A3; then (f1*s1).n<=f2.(s1.n) by A13,RFUNCT_2:
21;
   hence (f1*s1).n<=(f2*s1).n by A15,RFUNCT_2:21;
  end; hence thesis by A14,A16,SEQ_2:32;
 suppose A17: dom f2/\right_open_halfline(r)c=dom f1/\right_open_halfline(r) &
  for g st g in dom f2/\right_open_halfline(r) holds f1.g<=f2.g;
  defpred X[Nat,real number] means
   $1<$2 & $2 in dom f2/\right_open_halfline r;
  A18: now let n; consider g such that
  A19: n+abs(r)<g & g in dom f2 by A1,Def6;
   reconsider g as real number;
   take g; 0<=abs(r) by ABSVALUE:5; then
A20:  n+0<=n+abs(r) by REAL_1:55;
   A21: 0<=n by NAT_1:18; r<=abs(r) by ABSVALUE:11;
   then 0+r<=n+abs(r) by A21,REAL_1:55;
   then r<g by A19,AXIOMS:22; then g in {g2: r<g2};
   then g in right_open_halfline(r) by Def3;
   hence X[n,g] by A19,A20,AXIOMS:22,XBOOLE_0:def 3;
  end;
  consider s1 be Real_Sequence such that
  A22: for n holds X[n,s1.n] from RealSeqChoice(A18);
 deffunc U(Nat) = $1;
  consider s2 be Real_Sequence such that
  A23: for n holds s2.n=U(n) from ExRealSeq;
  A24: s2 is divergent_to+infty by A23,Th47;
    now let n; n<s1.n by A22; hence s2.n<=s1.n by A23;
  end; then A25: s1 is divergent_to+infty by A24,Th69;
  A26: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2;
  A27: rng s1 c=dom f2
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f2/\right_open_halfline(r) by A22;
   hence x in dom f2 by XBOOLE_0:def 3;
  end; then A28: f2*s1 is convergent & lim(f2*s1)=lim_in+infty f2
   by A1,A25,A26,Def12;
  A29: rng s1 c=dom f1
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f2/\right_open_halfline(r) by A22;
hence x in dom f1 by A17,XBOOLE_0:def 3;
  end; then A30: f1*s1 is convergent & lim(f1*s1)=lim_in+infty f1
   by A1,A25,A26,Def12;
    now let n; s1.n in dom f2/\right_open_halfline(r) by A22;
   then f1.(s1.n)<=f2.(s1.n) by A17; then (f1*s1).n<=f2.(s1.n) by A29,RFUNCT_2:
21;
   hence (f1*s1).n<=(f2*s1).n by A27,RFUNCT_2:21;
  end; hence thesis by A28,A30,SEQ_2:32;
 end; hence thesis;
end;

theorem
  f1 is convergent_in-infty & f2 is convergent_in-infty &
(ex r st ((dom f1 /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r) &
 for g st g in dom f1 /\ left_open_halfline(r) holds f1.g<=f2.g) or
 (dom f2 /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
 for g st g in dom f2 /\ left_open_halfline(r) holds f1.g<=f2.g))) implies
lim_in-infty f1<=lim_in-infty f2
proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty;
 given r such that
 A2: (dom f1/\left_open_halfline(r)c=dom f2/\left_open_halfline(r) &
 for g st g in dom f1/\left_open_halfline(r) holds f1.g<=f2.g) or
 (dom f2/\left_open_halfline(r)c=dom f1/\left_open_halfline(r) &
 for g st g in dom f2/\left_open_halfline(r) holds f1.g<=f2.g);
   now per cases by A2;
 suppose A3: dom f1/\left_open_halfline(r)c=dom f2/\left_open_halfline(r) &
  for g st g in dom f1/\left_open_halfline(r) holds f1.g<=f2.g;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f1/\left_open_halfline r;
  A4: now let n; consider g such that A5: g<-n-abs(r) & g in dom f1 by A1,Def9;
   reconsider g as real number;
   take g; 0<=abs(r) by ABSVALUE:5; then
  -n-abs(r)<=-n-0 by REAL_1:92;
   then
A6:  g < -n by A5,AXIOMS:22;
   A7: 0<=n by NAT_1:18; -abs(r)<=r by ABSVALUE:11;
   then -abs(r)-n<=r-0 by A7,REAL_1:92;
   then -n+-abs(r) <=r by XCMPLX_0:def 8;
   then -n-abs(r)<=r by XCMPLX_0:def 8
; then g<r by A5,AXIOMS:22; then g in {g2: g2<r};
   then g in left_open_halfline(r) by PROB_1:def 15;
   hence X[n,g] by A5,A6,XBOOLE_0:def 3;
  end; consider s1 be Real_Sequence such that
  A8: for n holds X[n,s1.n] from RealSeqChoice(A4);
 deffunc U(Nat) = -$1;
  consider s2 be Real_Sequence such that
  A9: for n holds s2.n=U(n) from ExRealSeq;
  A10: s2 is divergent_to-infty by A9,Th48;
    now let n; s1.n<-n by A8; hence s1.n<=s2.n by A9;
  end; then A11: s1 is divergent_to-infty by A10,Th70;
  A12: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2;
  A13: rng s1 c=dom f1
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f1/\left_open_halfline(r) by A8;
   hence x in dom f1 by XBOOLE_0:def 3;
  end; then A14: f1*s1 is convergent & lim(f1*s1)=lim_in-infty f1
    by A1,A11,A12,Def13;
  A15: rng s1 c=dom f2
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f1/\left_open_halfline(r) by A8;
hence x in dom f2 by A3,XBOOLE_0:def 3;
  end; then A16: f2*s1 is convergent & lim(f2*s1)=lim_in-infty f2
    by A1,A11,A12,Def13;
    now let n; s1.n in dom f1/\left_open_halfline(r) by A8;
   then f1.(s1.n)<=f2.(s1.n) by A3; then (f1*s1).n<=f2.(s1.n) by A13,RFUNCT_2:
21;
   hence (f1*s1).n<=(f2*s1).n by A15,RFUNCT_2:21;
  end; hence thesis by A14,A16,SEQ_2:32;
 suppose A17: dom f2/\left_open_halfline(r)c=dom f1/\left_open_halfline(r) &
  for g st g in dom f2/\left_open_halfline(r) holds f1.g<=f2.g;
  defpred X[Nat,real number] means
   $2<-$1 & $2 in dom f2/\left_open_halfline r;
  A18: now let n; consider g such that
  A19: g<-n-abs(r) & g in dom f2 by A1,Def9;
   reconsider g as real number;
   take g; 0<=abs(r) by ABSVALUE:5; then
A20:    -n-abs(r)<=-n-0 by REAL_1:92;
   A21: 0<=n by NAT_1:18; -abs(r)<=r by ABSVALUE:11;
   then -abs(r)-n<=r-0 by A21,REAL_1:92; then -n+-abs(r)<=r
 by XCMPLX_0:def 8;
   then -n-abs(r)<=r by XCMPLX_0:def 8
; then g<r by A19,AXIOMS:22; then g in {g2: g2<r};
   then g in left_open_halfline(r) by PROB_1:def 15;
   hence X[n,g] by A19,A20,AXIOMS:22,XBOOLE_0:def 3;
  end; consider s1 be Real_Sequence such that
  A22: for n holds X[n,s1.n] from RealSeqChoice(A18);
 deffunc U(Nat) = -$1;
  consider s2 be Real_Sequence such that
  A23: for n holds s2.n=U(n) from ExRealSeq;
  A24: s2 is divergent_to-infty by A23,Th48;
    now let n; s1.n<-n by A22; hence s1.n<=s2.n by A23;
  end; then A25: s1 is divergent_to-infty by A24,Th70;
  A26: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2;
  A27: rng s1 c=dom f2
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f2/\left_open_halfline(r) by A22;
   hence x in dom f2 by XBOOLE_0:def 3;
  end; then A28: f2*s1 is convergent & lim(f2*s1)=lim_in-infty f2
    by A1,A25,A26,Def13;
  A29: rng s1 c=dom f1
  proof let x be set; assume x in rng s1; then ex n st
 x=s1.n by RFUNCT_2:9; then x in dom f2/\left_open_halfline(r) by A22;
hence x in dom f1 by A17,XBOOLE_0:def 3;
  end; then A30: f1*s1 is convergent & lim(f1*s1)=lim_in-infty f1
    by A1,A25,A26,Def13;
    now let n; s1.n in dom f2/\left_open_halfline(r) by A22;
   then f1.(s1.n)<=f2.(s1.n) by A17; then (f1*s1).n<=f2.(s1.n) by A29,RFUNCT_2:
21;
   hence (f1*s1).n<=(f2*s1).n by A27,RFUNCT_2:21;
  end; hence thesis by A28,A30,SEQ_2:32;
 end; hence thesis;
end;

theorem
  (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) &
(for r ex g st r<g & g in dom f & f.g<>0) implies f^ is convergent_in+infty &
lim_in+infty(f^)=0
proof assume that A1: f is divergent_in+infty_to+infty or
  f is divergent_in+infty_to-infty
 and A2:  for r ex g st r<g & g in dom f & f.g<>0;
 A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8;
 A4: now let r; consider g such that A5: r<g & g in dom f & f.g<>0 by A2;
  take g; not f.g in {0} by A5,TARSKI:def 1;
  then not g in f"{0} by FUNCT_1:def 13;
  hence r<g & g in dom(f^) by A3,A5,XBOOLE_0:def 4;
 end;
   now per cases by A1;
 suppose A6: f is divergent_in+infty_to+infty;
  A7: now let seq such that A8: seq is divergent_to+infty & rng seq c=dom(f^);
     dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A8,XBOOLE_1:1
;
    then f*seq is divergent_to+infty by A6,A8,Def7;
   then (f*seq)" is convergent & lim((f*seq)")=0 by Th61;
   hence (f^)*seq is convergent & lim((f^)*seq)=0 by A8,RFUNCT_2:27;
  end; hence f^ is convergent_in+infty by A4,Def6; hence thesis by A7,Def12;
 suppose A9: f is divergent_in+infty_to-infty;
  A10: now let seq such that A11: seq is divergent_to+infty & rng seq c=dom(f^)
;
     dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A11,XBOOLE_1:1
;
    then f*seq is divergent_to-infty by A9,A11,Def8;
   then (f*seq)" is convergent & lim((f*seq)")=0 by Th61;
   hence (f^)*seq is convergent & lim((f^)*seq)=0 by A11,RFUNCT_2:27;
  end; hence f^ is convergent_in+infty by A4,Def6; hence thesis by A10,Def12;
 end; hence thesis;
end;

theorem
  (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) &
(for r ex g st g<r & g in dom f & f.g<>0) implies f^ is convergent_in-infty &
lim_in-infty(f^)=0
proof assume that
 A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty
 and A2:  for r ex g st g<r & g in dom f & f.g<>0;
 A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8;
 A4: now let r; consider g such that A5: g<r & g in dom f & f.g<>0 by A2;
  take g; not f.g in {0} by A5,TARSKI:def 1;
  then not g in f"{0} by FUNCT_1:def 13;
  hence g<r & g in dom(f^) by A3,A5,XBOOLE_0:def 4;
 end;
   now per cases by A1;
 suppose A6: f is divergent_in-infty_to+infty;
  A7: now let seq such that A8: seq is divergent_to-infty & rng seq c=dom(f^);
     dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A8,XBOOLE_1:1
;
    then f*seq is divergent_to+infty by A6,A8,Def10;
   then (f*seq)" is convergent & lim((f*seq)")=0 by Th61;
   hence (f^)*seq is convergent & lim((f^)*seq)=0 by A8,RFUNCT_2:27;
  end; hence f^ is convergent_in-infty by A4,Def9; hence thesis by A7,Def13;
 suppose A9: f is divergent_in-infty_to-infty;
  A10: now let seq such that A11: seq is divergent_to-infty & rng seq c=dom(f^)
;
     dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A11,XBOOLE_1:1
;
    then f*seq is divergent_to-infty by A9,A11,Def11;
   then (f*seq)" is convergent & lim((f*seq)")=0 by Th61;
   hence (f^)*seq is convergent & lim((f^)*seq)=0 by A11,RFUNCT_2:27;
  end; hence f^ is convergent_in-infty by A4,Def9; hence thesis by A10,Def13;
 end; hence thesis;
end;

theorem
  f is convergent_in+infty & lim_in+infty f=0 &
(for r ex g st r<g & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<=f.g) implies
f^ is divergent_in+infty_to+infty
proof assume A1: f is convergent_in+infty & lim_in+infty f=0 &
 for r ex g st r<g & g in dom f & f.g<>0;
 given r such that A2: for g st g in dom f/\
right_open_halfline(r) holds 0<=f.g;
 thus for r1 ex g1 st r1<g1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f & f.g1<>0 by A1;
  take g1; thus r1<g1 by A3; not f.g1 in {0} by A3,TARSKI:def 1;
  then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0
:def 4;
  hence thesis by RFUNCT_1:def 8;
 end;
 let s be Real_Sequence;
 assume A4: s is divergent_to+infty & rng s c=dom(f^);
 then consider k such that A5: for n st k<=n holds r<s.n by Def4;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A6: s^\k is divergent_to+infty by A4,Th53;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1;
 then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def12;
 A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26;
 A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then r<s.(n+k) by A5;
  then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2};
  then (s^\k).n in right_open_halfline(r) by Def3;
  then (s^\k).n in dom f/\right_open_halfline(r) by A8,A12,XBOOLE_0:def 3;
then A13: 0<=
f.((s^\k).n)
     by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7;
  hence 0<(f*(s^\k)).n by A8,A13,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A14: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies 0<(f*(s^\k)).n by A11;
 then A15: (f*(s^\k))" is divergent_to+infty by A9,A14,Th62;
   (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34;
end;

theorem
  f is convergent_in+infty & lim_in+infty f=0 &
(for r ex g st r<g & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<=0) implies
f^ is divergent_in+infty_to-infty
proof assume A1: f is convergent_in+infty & lim_in+infty f=0 &
 for r ex g st r<g & g in dom f & f.g<>0; given r such that
 A2: for g st g in dom f/\right_open_halfline(r) holds f.g<=0;
 thus for r1 ex g1 st r1<g1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f & f.g1<>0 by A1;
  take g1; thus r1<g1 by A3; not f.g1 in {0} by A3,TARSKI:def 1;
  then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0
:def 4;
  hence thesis by RFUNCT_1:def 8;
 end;
 let s be Real_Sequence;
 assume A4: s is divergent_to+infty & rng s c=dom(f^);
 then consider k such that A5: for n st k<=n holds r<s.n by Def4;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A6: s^\k is divergent_to+infty by A4,Th53;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1;
 then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def12;
 A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26;
 A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then r<s.(n+k) by A5;
  then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2};
  then (s^\k).n in right_open_halfline(r) by Def3;
  then (s^\k).n in dom f/\right_open_halfline(r) by A8,A12,XBOOLE_0:def 3;
  then A13: f.((s^\k).n)<=0 by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7;
  hence (f*(s^\k)).n<0 by A8,A13,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A14: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies (f*(s^\k)).n<0 by A11;
 then A15: (f*(s^\k))" is divergent_to-infty by A9,A14,Th63;
   (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34;
end;

theorem
  f is convergent_in-infty & lim_in-infty f=0 &
(for r ex g st g<r & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<=f.g) implies
f^ is divergent_in-infty_to+infty
proof assume A1: f is convergent_in-infty & lim_in-infty f=0 &
 for r ex g st g<r & g in dom f & f.g<>0;
 given r such that A2: for g st g in dom f/\left_open_halfline(r) holds 0<=f.g;
 thus for r1 ex g1 st g1<r1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f & f.g1<>0 by A1;
  take g1; thus g1<r1 by A3; not f.g1 in {0} by A3,TARSKI:def 1;
  then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0
:def 4;
  hence thesis by RFUNCT_1:def 8;
 end;
 let s be Real_Sequence; assume A4: s is divergent_to-infty & rng s c=dom (f^);
 then consider k such that A5: for n st k<=n holds s.n<r by Def5;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A6: s^\k is divergent_to-infty by A4,Th54;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A7: rng s c=dom f by A4,XBOOLE_1:1;
   rng(s^\k)c=rng s by RFUNCT_2:7;
 then A8: rng(s^\k)c=dom (f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1;
 then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def13;
 A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26;
 A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then s.(n+k)<r by A5;
  then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r};
  then (s^\k).n in left_open_halfline(r) by PROB_1:def 15;
  then (s^\k).n in dom f/\left_open_halfline(r) by A8,A12,XBOOLE_0:def 3
; then A13: 0<=f.((s^\k).n) by A2; 0<>(f*(s^\k)).n by A10,SEQ_1:7;
  hence 0<(f*(s^\k)).n by A8,A13,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A14: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies 0<(f*(s^\k)).n by A11;
 then A15: (f*(s^\k))" is divergent_to+infty by A9,A14,Th62;
   (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34;
end;

theorem
  f is convergent_in-infty & lim_in-infty f=0 &
(for r ex g st g<r & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<=0) implies
f^ is divergent_in-infty_to-infty
proof assume A1: f is convergent_in-infty & lim_in-infty f=0 &
 for r ex g st g<r & g in dom f & f.g<>0;
 given r such that A2: for g st g in dom f/\left_open_halfline(r) holds f.g<=0;
 thus for r1 ex g1 st g1<r1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f & f.g1<>0 by A1;
  take g1; thus g1<r1 by A3; not f.g1 in {0} by A3,TARSKI:def 1;
  then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0
:def 4;
  hence thesis by RFUNCT_1:def 8;
 end;
 let s be Real_Sequence;
 assume A4: s is divergent_to-infty & rng s c=dom (f^);
 then consider k such that A5: for n st k<=n holds s.n<r by Def5;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A6: s^\k is divergent_to-infty by A4,Th54;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1;
 then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def13;
 A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26;
 A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then s.(n+k)<r by A5;
  then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r};
  then (s^\k).n in left_open_halfline(r) by PROB_1:def 15;
  then (s^\k).n in dom f/\left_open_halfline(r) by A8,A12,XBOOLE_0:def 3
; then A13: f.((s^\k).n)<=0 by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7;
  hence (f*(s^\k)).n<0 by A8,A13,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A14: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies (f*(s^\k)).n<0 by A11;
 then A15: (f*(s^\k))" is divergent_to-infty by A9,A14,Th63;
   (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34;
end;

theorem
  f is convergent_in+infty & lim_in+infty f=0 &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<f.g) implies
f^ is divergent_in+infty_to+infty
proof assume A1: f is convergent_in+infty & lim_in+infty f=0;
 given r such that A2: for g st g in dom f/\right_open_halfline(r) holds 0<f.g;
 thus for r1 ex g1 st r1<g1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f by A1,Def6;
    now per cases;
  suppose A4: g1<=r; consider g2 such that A5: r<g2 & g2 in dom f by A1,Def6
; take g2;
     g1<g2 by A4,A5,AXIOMS:22;
   hence r1<g2 by A3,AXIOMS:22; g2 in {r2: r<r2} by A5;
   then g2 in right_open_halfline(r) by Def3;
   then g2 in dom f/\right_open_halfline(r) by A5,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  suppose A6: r<=g1; consider g2 such that A7: g1<g2 & g2 in dom f by A1,Def6
; take g2;
   thus r1<g2 by A3,A7,AXIOMS:22; r<g2 by A6,A7,AXIOMS:22;
   then g2 in {r2: r<r2}; then g2 in right_open_halfline(r) by Def3;
   then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  end; hence thesis;
 end;
 let s be Real_Sequence; assume A8: s is divergent_to+infty & rng s c=dom (f^);
 then consider k such that A9: for n st k<=n holds r<s.n by Def4;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A10: s^\k is divergent_to+infty by A8,Th53;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1;
 then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def12;
 A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then r<s.(n+k) by A9;
  then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2};
  then (s^\k).n in right_open_halfline(r) by Def3;
  then (s^\k).n in dom f/\right_open_halfline(r) by A12,A15,XBOOLE_0:def 3;
  then 0<f.((s^\k).n) by A2;
  hence 0<(f*(s^\k)).n by A12,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A16: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies 0<(f*(s^\k)).n by A14;
 then A17: (f*(s^\k))" is divergent_to+infty by A13,A16,Th62;
   (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34;
end;

theorem
  f is convergent_in+infty & lim_in+infty f=0 &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<0) implies
f^ is divergent_in+infty_to-infty
proof assume A1: f is convergent_in+infty & lim_in+infty f=0;
 given r such that A2: for g st g in dom f/\right_open_halfline(r) holds f.g<0;
 thus for r1 ex g1 st r1<g1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f by A1,Def6;
    now per cases;
  suppose A4: g1<=r; consider g2 such that A5: r<g2 & g2 in dom f by A1,Def6
; take g2;
     g1<g2 by A4,A5,AXIOMS:22; hence r1<g2 by A3,AXIOMS:22;
     g2 in {r2: r<r2} by A5; then g2 in right_open_halfline(r) by Def3;
   then g2 in dom f/\right_open_halfline(r) by A5,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  suppose A6: r<=g1; consider g2 such that A7: g1<g2 & g2 in dom f by A1,Def6
; take g2;
   thus r1<g2 by A3,A7,AXIOMS:22; r<g2 by A6,A7,AXIOMS:22;
   then g2 in {r2: r<r2}; then g2 in right_open_halfline(r) by Def3;
   then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  end; hence thesis;
 end;
 let s be Real_Sequence; assume A8: s is divergent_to+infty & rng s c=dom (f^);
 then consider k such that A9: for n st k<=n holds r<s.n by Def4;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A10: s^\k is divergent_to+infty by A8,Th53;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1;
 then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def12;
 A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then r<s.(n+k) by A9;
  then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2};
  then (s^\k).n in right_open_halfline(r) by Def3;
  then (s^\k).n in dom f/\right_open_halfline(r) by A12,A15,XBOOLE_0:def 3;
  then f.((s^\k).n)<0
    by A2;
  hence (f*(s^\k)).n<0 by A12,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A16: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies (f*(s^\k)).n<0 by A14;
 then A17: (f*(s^\k))" is divergent_to-infty by A13,A16,Th63;
   (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A8,RFUNCT_2:27;
 hence (f^)*s is divergent_to-infty by A17,Th34;
end;

theorem
  f is convergent_in-infty & lim_in-infty f=0 &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<f.g) implies
f^ is divergent_in-infty_to+infty
proof assume A1: f is convergent_in-infty & lim_in-infty f=0;
 given r such that A2: for g st g in dom f/\left_open_halfline(r) holds 0<f.g;
 thus for r1 ex g1 st g1<r1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f by A1,Def9;
    now per cases;
  suppose A4: g1<=r; consider g2 such that A5: g2<g1 & g2 in dom f by A1,Def9
; take g2;
   thus g2<r1 by A3,A5,AXIOMS:22; g2<r by A4,A5,AXIOMS:22;
   then g2 in {r2: r2<r}; then g2 in left_open_halfline(r) by PROB_1:def 15;
   then g2 in dom f/\left_open_halfline(r) by A5,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  suppose A6: r<=g1; consider g2 such that A7: g2<r & g2 in dom f by A1,Def9
; take g2;
     g2<g1 by A6,A7,AXIOMS:22; hence g2<r1 by A3,AXIOMS:22;
     g2 in {r2: r2<r} by A7;
   then g2 in left_open_halfline(r) by PROB_1:def 15;
   then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  end; hence thesis;
 end;
 let s be Real_Sequence; assume A8: s is divergent_to-infty & rng s c=dom (f^);
 then consider k such that A9: for n st k<=n holds s.n<r by Def5;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A10: s^\k is divergent_to-infty by A8,Th54;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1;
 then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def13;
 A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then s.(n+k)<r by A9;
  then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r};
  then (s^\k).n in left_open_halfline(r) by PROB_1:def 15;
  then (s^\k).n in dom f/\left_open_halfline(r) by A12,A15,XBOOLE_0:def 3
; then 0<f.((s^\k).n) by A2;
  hence 0<(f*(s^\k)).n by A12,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A16: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies 0<(f*(s^\k)).n by A14;
 then A17: (f*(s^\k))" is divergent_to+infty by A13,A16,Th62;
   (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34;
end;

theorem
  f is convergent_in-infty & lim_in-infty f=0 &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<0) implies
f^ is divergent_in-infty_to-infty
proof assume A1: f is convergent_in-infty & lim_in-infty f=0;
 given r such that A2: for g st g in dom f/\left_open_halfline(r) holds f.g<0;
 thus for r1 ex g1 st g1<r1 & g1 in dom(f^)
 proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f by A1,Def9;
    now per cases;
  suppose A4: g1<=r; consider g2 such that A5: g2<g1 & g2 in dom f by A1,Def9
; take g2;
   thus g2<r1 by A3,A5,AXIOMS:22; g2<r by A4,A5,AXIOMS:22;
   then g2 in {r2: r2<r}; then g2 in left_open_halfline(r) by PROB_1:def 15;
   then g2 in dom f/\left_open_halfline(r) by A5,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  suppose A6: r<=g1; consider g2 such that A7: g2<r & g2 in dom f by A1,Def9
; take g2;
     g2<g1 by A6,A7,AXIOMS:22;
   hence g2<r1 by A3,AXIOMS:22; g2 in {r2: r2<r} by A7;
   then g2 in left_open_halfline(r) by PROB_1:def 15;
   then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 3;
   then 0<>f.g2 by A2
; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13;
   then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4;
   hence g2 in dom(f^) by RFUNCT_1:def 8;
  end; hence thesis;
 end;
 let s be Real_Sequence; assume A8: s is divergent_to-infty & rng s c=dom (f^);
 then consider k such that A9: for n st k<=n holds s.n<r by Def5;
   s^\k is_subsequence_of s by SEQM_3:47;
 then A10: s^\k is divergent_to-infty by A8,Th54;
   dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
 then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
 then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1;
 then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def13;
 A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37
; then s.(n+k)<r by A9;
  then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r};
  then (s^\k).n in left_open_halfline(r) by PROB_1:def 15;
  then (s^\k).n in dom f/\left_open_halfline(r) by A12,A15,XBOOLE_0:def 3
; then f.((s^\k).n)<0 by A2;
  hence (f*(s^\k)).n<0 by A12,RFUNCT_2:21;
 end; then for n holds 0<>(f*(s^\k)).n;
 then A16: f*(s^\k) is_not_0 by SEQ_1:7;
   for n holds 0<=n implies (f*(s^\k)).n<0 by A14;
 then A17: (f*(s^\k))" is divergent_to-infty by A13,A16,Th63;
   (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22
 .=((f*s)")^\k by SEQM_3:41
 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34;
end;

Back to top