:: TOPRNS_1 semantic presentation

begin

definition
let N be Nat;
mode Real_Sequence of N is sequence of (TOP-REAL N);
end;


theorem Th1: :: TOPRNS_1:1
for N being Element of NAT
for f being Function holds
( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) )
proof
let N be Element of NAT ; ::_thesis: for f being Function holds
( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) )
let f be Function; ::_thesis: ( f is Real_Sequence of N iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) )
thus  ( f is Real_Sequence of N implies ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) ) ) by NORMSP_1:12; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is Point of (TOP-REAL N) ) implies f is Real_Sequence of N )
assume that
A1: dom f = NAT and
A2: for n being Element of NAT holds f . n is Point of (TOP-REAL N) ; ::_thesis: f is Real_Sequence of N
 for x being set st x in NAT holds
f . x is Point of (TOP-REAL N) by A2;
hence  f is Real_Sequence of N by A1, NORMSP_1:12; ::_thesis: verum
end;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is non-zero  means :Def1: :: TOPRNS_1:def 1
 rng IT c= NonZero (TOP-REAL N);
end;

:: deftheorem Def1 defines non-zero TOPRNS_1:def_1_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is non-zero iff rng IT c= NonZero (TOP-REAL N) );

theorem Th2: :: TOPRNS_1:2
for N being Element of NAT
for seq being Real_Sequence of N holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) )
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) )
let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) )
thus  ( seq is non-zero implies for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ) ::_thesis: ( ( for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ) implies seq is non-zero )
proof
assume  seq is non-zero ; ::_thesis: for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N)
then A1: rng seq c= NonZero (TOP-REAL N) by Def1;
let x be set ; ::_thesis: ( x in NAT implies seq . x <> 0. (TOP-REAL N) )
assume  x in NAT ; ::_thesis: seq . x <> 0. (TOP-REAL N)
then  x in dom seq by Th1;
then  seq . x in rng seq by FUNCT_1:def_3;
then  not seq . x in {(0. (TOP-REAL N))} by A1, XBOOLE_0:def_5;
hence  seq . x <> 0. (TOP-REAL N) by TARSKI:def_1; ::_thesis: verum
end;
assume A2: for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ; ::_thesis: seq is non-zero
now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_
y_in_NonZero_(TOP-REAL_N)
let y be set ; ::_thesis: ( y in rng seq implies y in NonZero (TOP-REAL N) )
assume  y in rng seq ; ::_thesis: y in NonZero (TOP-REAL N)
then consider x being set  such that
A3: x in dom seq and
A4: seq . x = y by FUNCT_1:def_3;
A5: x in NAT by A3, NORMSP_1:12;
then  y <> 0. (TOP-REAL N) by A2, A4;
then A6: not y in {(0. (TOP-REAL N))} by TARSKI:def_1;
 y is Point of (TOP-REAL N) by A4, A5, NORMSP_1:12;
hence  y in NonZero (TOP-REAL N) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then  rng seq c= NonZero (TOP-REAL N) by TARSKI:def_3;
hence  seq is non-zero by Def1; ::_thesis: verum
end;

theorem Th3: :: TOPRNS_1:3
for N being Element of NAT
for seq being Real_Sequence of N holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) )
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) )
let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero iff for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) )
thus  ( seq is non-zero implies for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) by Th2; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ) implies seq is non-zero )
assume  for n being Element of NAT holds seq . n <> 0. (TOP-REAL N) ; ::_thesis: seq is non-zero
then  for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) ;
hence  seq is non-zero by Th2; ::_thesis: verum
end;

definition
let N be Nat;
let seq1, seq2 be Real_Sequence of N;
funcseq1 + seq2 ->  Real_Sequence of N equals :: TOPRNS_1:def 2
seq1 + seq2;
coherence
 seq1 + seq2 is Real_Sequence of N
proof
A1: ( dom seq1 = NAT & dom seq2 = NAT ) by FUNCT_2:def_1;
 dom (seq1 + seq2) = (dom seq1) /\ (dom seq2) by VFUNCT_1:def_1;
hence  seq1 + seq2 is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum
end;
end;

:: deftheorem  defines + TOPRNS_1:def_2_:_
 for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq1 + seq2;

definition
let r be Real;
let N be Nat;
let seq be Real_Sequence of N;
funcr * seq ->  Real_Sequence of N equals :: TOPRNS_1:def 3
r (#) seq;
coherence
 r (#) seq is Real_Sequence of N
proof
A1: dom seq = NAT by FUNCT_2:def_1;
 dom (r (#) seq) = dom seq by VFUNCT_1:def_4;
hence  r (#) seq is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum
end;
end;

:: deftheorem  defines * TOPRNS_1:def_3_:_
 for r being Real
for N being Nat
for seq being Real_Sequence of N holds r * seq = r (#) seq;

definition
let N be Nat;
let seq be Real_Sequence of N;
func - seq ->  Real_Sequence of N equals :: TOPRNS_1:def 4
 - seq;
coherence
 - seq is Real_Sequence of N
proof
A1: dom seq = NAT by FUNCT_2:def_1;
 dom (- seq) = dom seq by VFUNCT_1:def_5;
hence  - seq is Real_Sequence of N by A1, FUNCT_2:67; ::_thesis: verum
end;
end;

:: deftheorem  defines - TOPRNS_1:def_4_:_
 for N being Nat
for seq being Real_Sequence of N holds - seq = - seq;

definition
let N be Nat;
let seq1, seq2 be Real_Sequence of N;
funcseq1 - seq2 ->  Real_Sequence of N equals :: TOPRNS_1:def 5
seq1 + (- seq2);
correctness
coherence
seq1 + (- seq2) is Real_Sequence of N;
;
end;

:: deftheorem  defines - TOPRNS_1:def_5_:_
 for N being Nat
for seq1, seq2 being Real_Sequence of N holds seq1 - seq2 = seq1 + (- seq2);

definition
let N be Nat;
let seq be Real_Sequence of N;
func|.seq.| ->  Real_Sequence means :Def6: :: TOPRNS_1:def 6
 for n being Element of NAT holds it . n = |.(seq . n).|;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = |.(seq . n).|
proof
deffunc H1( Element of NAT ) ->  Element of REAL = |.(seq . $1).|;
thus  ex s being Real_Sequence st
for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = |.(seq . n).| ) & ( for n being Element of NAT holds b2 . n = |.(seq . n).| ) holds
b1 = b2
proof
let seq8, seq9 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq8 . n = |.(seq . n).| ) & ( for n being Element of NAT holds seq9 . n = |.(seq . n).| ) implies seq8 = seq9 )
assume that
A1: for n being Element of NAT holds seq8 . n = |.(seq . n).| and
A2: for n being Element of NAT holds seq9 . n = |.(seq . n).| ; ::_thesis: seq8 = seq9
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: seq8 . n = seq9 . n
 seq9 . n = |.(seq . n).| by A2;
hence  seq8 . n = seq9 . n by A1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines |. TOPRNS_1:def_6_:_
 for N being Nat
for seq being Real_Sequence of N
for b3 being Real_Sequence holds
( b3 = |.seq.| iff for n being Element of NAT holds b3 . n = |.(seq . n).| );

theorem Th4: :: TOPRNS_1:4
for N, n being Nat
for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
proof
let N, n be Nat; ::_thesis: for seq1, seq2 being Real_Sequence of N holds (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
let seq1, seq2 be Real_Sequence of N; ::_thesis: (seq1 + seq2) . n = (seq1 . n) + (seq2 . n)
reconsider m = n as Element of NAT by ORDINAL1:def_12;
A1: dom (seq1 + seq2) = NAT by FUNCT_2:def_1;
thus (seq1 + seq2) . n = (seq1 + seq2) /. m
.= (seq1 /. m) + (seq2 /. m) by A1, VFUNCT_1:def_1
.= (seq1 . n) + (seq2 . n) ; ::_thesis: verum
end;

theorem Th5: :: TOPRNS_1:5
for r being Real
for N, n being Nat
for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
proof
let r be Real; ::_thesis: for N, n being Nat
for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
let N, n be Nat; ::_thesis: for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
let seq be Real_Sequence of N; ::_thesis: (r * seq) . n = r * (seq . n)
reconsider m = n as Element of NAT by ORDINAL1:def_12;
A1: dom (r * seq) = NAT by FUNCT_2:def_1;
thus (r * seq) . n = (r * seq) /. m
.= r * (seq /. m) by A1, VFUNCT_1:def_4
.= r * (seq . n) ; ::_thesis: verum
end;

theorem Th6: :: TOPRNS_1:6
for N, n being Nat
for seq being Real_Sequence of N holds (- seq) . n = - (seq . n)
proof
let N, n be Nat; ::_thesis: for seq being Real_Sequence of N holds (- seq) . n = - (seq . n)
let seq be Real_Sequence of N; ::_thesis: (- seq) . n = - (seq . n)
reconsider m = n as Element of NAT by ORDINAL1:def_12;
A1: dom (- seq) = NAT by FUNCT_2:def_1;
thus (- seq) . n = (- seq) /. m
.= - (seq /. m) by A1, VFUNCT_1:def_5
.= - (seq . n) ; ::_thesis: verum
end;

theorem Th7: :: TOPRNS_1:7
for N being Element of NAT
for r being Real
for w being Point of (TOP-REAL N) holds (abs r) * |.w.| = |.(r * w).| by EUCLID:11;

theorem :: TOPRNS_1:8
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.|
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.|
let r be Real; ::_thesis: for seq being Real_Sequence of N holds |.(r * seq).| = (abs r) (#) |.seq.|
let seq be Real_Sequence of N; ::_thesis: |.(r * seq).| = (abs r) (#) |.seq.|
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: |.(r * seq).| . n = ((abs r) (#) |.seq.|) . n
thus |.(r * seq).| . n = |.((r * seq) . n).| by Def6
.= |.(r * (seq . n)).| by Th5
.= (abs r) * |.(seq . n).| by Th7
.= (abs r) * (|.seq.| . n) by Def6
.= ((abs r) (#) |.seq.|) . n by SEQ_1:9 ; ::_thesis: verum
end;

theorem :: TOPRNS_1:9
for N being Element of NAT
for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1
proof
let N be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence of N holds seq1 + seq2 = seq2 + seq1
let seq1, seq2 be Real_Sequence of N; ::_thesis: seq1 + seq2 = seq2 + seq1
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (seq1 + seq2) . n = (seq2 + seq1) . n
thus (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) by Th4
.= (seq2 + seq1) . n by Th4 ; ::_thesis: verum
end;

theorem Th10: :: TOPRNS_1:10
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof
let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((seq1 + seq2) + seq3) . n = (seq1 + (seq2 + seq3)) . n
thus ((seq1 + seq2) + seq3) . n = ((seq1 + seq2) . n) + (seq3 . n) by Th4
.= ((seq1 . n) + (seq2 . n)) + (seq3 . n) by Th4
.= (seq1 . n) + ((seq2 . n) + (seq3 . n)) by EUCLID:26
.= (seq1 . n) + ((seq2 + seq3) . n) by Th4
.= (seq1 + (seq2 + seq3)) . n by Th4 ; ::_thesis: verum
end;

theorem Th11: :: TOPRNS_1:11
for N being Element of NAT
for seq being Real_Sequence of N holds - seq = (- 1) * seq
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds - seq = (- 1) * seq
let seq be Real_Sequence of N; ::_thesis: - seq = (- 1) * seq
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (- seq) . n = ((- 1) * seq) . n
thus ((- 1) * seq) . n = (- 1) * (seq . n) by Th5
.= - (seq . n) by EUCLID:39
.= (- seq) . n by Th6 ; ::_thesis: verum
end;

theorem Th12: :: TOPRNS_1:12
for N being Element of NAT
for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
let r be Real; ::_thesis: for seq1, seq2 being Real_Sequence of N holds r * (seq1 + seq2) = (r * seq1) + (r * seq2)
let seq1, seq2 be Real_Sequence of N; ::_thesis: r * (seq1 + seq2) = (r * seq1) + (r * seq2)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (r * (seq1 + seq2)) . n = ((r * seq1) + (r * seq2)) . n
thus (r * (seq1 + seq2)) . n = r * ((seq1 + seq2) . n) by Th5
.= r * ((seq1 . n) + (seq2 . n)) by Th4
.= (r * (seq1 . n)) + (r * (seq2 . n)) by EUCLID:32
.= ((r * seq1) . n) + (r * (seq2 . n)) by Th5
.= ((r * seq1) . n) + ((r * seq2) . n) by Th5
.= ((r * seq1) + (r * seq2)) . n by Th4 ; ::_thesis: verum
end;

theorem Th13: :: TOPRNS_1:13
for N being Element of NAT
for r, q being Real
for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
proof
let N be Element of NAT ; ::_thesis: for r, q being Real
for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
let r, q be Real; ::_thesis: for seq being Real_Sequence of N holds (r * q) * seq = r * (q * seq)
let seq be Real_Sequence of N; ::_thesis: (r * q) * seq = r * (q * seq)
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: ((r * q) * seq) . n = (r * (q * seq)) . n
thus ((r * q) * seq) . n = (r * q) * (seq . n) by Th5
.= r * (q * (seq . n)) by EUCLID:30
.= r * ((q * seq) . n) by Th5
.= (r * (q * seq)) . n by Th5 ; ::_thesis: verum
end;

theorem Th14: :: TOPRNS_1:14
for N being Element of NAT
for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)
let r be Real; ::_thesis: for seq1, seq2 being Real_Sequence of N holds r * (seq1 - seq2) = (r * seq1) - (r * seq2)
let seq1, seq2 be Real_Sequence of N; ::_thesis: r * (seq1 - seq2) = (r * seq1) - (r * seq2)
thus r * (seq1 - seq2) = (r * seq1) + (r * (- seq2)) by Th12
.= (r * seq1) + (r * ((- 1) * seq2)) by Th11
.= (r * seq1) + (((- 1) * r) * seq2) by Th13
.= (r * seq1) + ((- 1) * (r * seq2)) by Th13
.= (r * seq1) - (r * seq2) by Th11 ; ::_thesis: verum
end;

theorem :: TOPRNS_1:15
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof
let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
thus seq1 - (seq2 + seq3) = seq1 + ((- 1) * (seq2 + seq3)) by Th11
.= seq1 + (((- 1) * seq2) + ((- 1) * seq3)) by Th12
.= seq1 + ((- seq2) + ((- 1) * seq3)) by Th11
.= seq1 + ((- seq2) + (- seq3)) by Th11
.= (seq1 - seq2) - seq3 by Th10 ; ::_thesis: verum
end;

theorem Th16: :: TOPRNS_1:16
for N being Element of NAT
for seq being Real_Sequence of N holds 1 * seq = seq
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds 1 * seq = seq
let seq be Real_Sequence of N; ::_thesis: 1 * seq = seq
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (1 * seq) . n = seq . n
thus (1 * seq) . n = 1 * (seq . n) by Th5
.= seq . n by EUCLID:29 ; ::_thesis: verum
end;

theorem Th17: :: TOPRNS_1:17
for N being Element of NAT
for seq being Real_Sequence of N holds - (- seq) = seq
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N holds - (- seq) = seq
let seq be Real_Sequence of N; ::_thesis: - (- seq) = seq
thus  - (- seq) = (- 1) * (- seq) by Th11
.= (- 1) * ((- 1) * seq) by Th11
.= ((- 1) * (- 1)) * seq by Th13
.= seq by Th16 ; ::_thesis: verum
end;

theorem :: TOPRNS_1:18
for N being Element of NAT
for seq1, seq2 being Real_Sequence of N holds seq1 - (- seq2) = seq1 + seq2 by Th17;

theorem :: TOPRNS_1:19
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof
let N be Element of NAT ; ::_thesis: for seq1, seq2, seq3 being Real_Sequence of N holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
let seq1, seq2, seq3 be Real_Sequence of N; ::_thesis: seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
thus seq1 - (seq2 - seq3) = seq1 + ((- 1) * (seq2 - seq3)) by Th11
.= seq1 + (((- 1) * seq2) - ((- 1) * seq3)) by Th14
.= seq1 + ((- seq2) - ((- 1) * seq3)) by Th11
.= seq1 + ((- seq2) - (- seq3)) by Th11
.= seq1 + ((- seq2) + seq3) by Th17
.= (seq1 - seq2) + seq3 by Th10 ; ::_thesis: verum
end;

theorem :: TOPRNS_1:20
for N being Element of NAT
for seq1, seq2, seq3 being Real_Sequence of N holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th10;

theorem Th21: :: TOPRNS_1:21
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero
let r be Real; ::_thesis: for seq being Real_Sequence of N st r <> 0 & seq is non-zero holds
r * seq is non-zero
let seq be Real_Sequence of N; ::_thesis: ( r <> 0 & seq is non-zero implies r * seq is non-zero )
assume that
A1: r <> 0 and
A2: seq is non-zero and
A3: not r * seq is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT  such that
A4: (r * seq) . n1 = 0. (TOP-REAL N) by A3, Th3;
A5: seq . n1 <> 0. (TOP-REAL N) by A2, Th3;
 r * (seq . n1) = 0. (TOP-REAL N) by A4, Th5;
hence  contradiction by A1, A5, EUCLID:31; ::_thesis: verum
end;

theorem :: TOPRNS_1:22
for N being Element of NAT
for seq being Real_Sequence of N st seq is non-zero holds
- seq is non-zero
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is non-zero holds
- seq is non-zero
let seq be Real_Sequence of N; ::_thesis: ( seq is non-zero implies - seq is non-zero )
assume  seq is non-zero ; ::_thesis: - seq is non-zero
then  (- 1) * seq is non-zero by Th21;
hence  - seq is non-zero by Th11; ::_thesis: verum
end;

theorem Th23: :: TOPRNS_1:23
for N being Element of NAT holds |.(0. (TOP-REAL N)).| = 0
proof
let N be Element of NAT ; ::_thesis: |.(0. (TOP-REAL N)).| = 0
thus |.(0. (TOP-REAL N)).| = |.(0* N).| by EUCLID:70
.= 0 by EUCLID:7 ; ::_thesis: verum
end;

theorem Th24: :: TOPRNS_1:24
for N being Element of NAT
for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0. (TOP-REAL N)
proof
let N be Element of NAT ; ::_thesis: for w being Point of (TOP-REAL N) st |.w.| = 0 holds
w = 0. (TOP-REAL N)
let w be Point of (TOP-REAL N); ::_thesis: ( |.w.| = 0 implies w = 0. (TOP-REAL N) )
reconsider s = w as Element of REAL N by EUCLID:22;
assume  |.w.| = 0 ; ::_thesis: w = 0. (TOP-REAL N)
then s = 0* N by EUCLID:8
.= 0. (TOP-REAL N) by EUCLID:70 ;
hence  w = 0. (TOP-REAL N) ; ::_thesis: verum
end;

theorem :: TOPRNS_1:25
for N being Element of NAT
for w being Point of (TOP-REAL N) holds |.w.| >= 0 ;

theorem :: TOPRNS_1:26
for N being Element of NAT
for w being Point of (TOP-REAL N) holds |.(- w).| = |.w.| by EUCLID:71;

theorem Th27: :: TOPRNS_1:27
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).|
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| = |.(w2 - w1).|
let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| = |.(w2 - w1).|
thus |.(w1 - w2).| = |.(- (w1 - w2)).| by EUCLID:71
.= |.(w2 - w1).| by EUCLID:44 ; ::_thesis: verum
end;

Lm1:  for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds
w1 = w2
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st |.(w1 - w2).| = 0 holds
w1 = w2
let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( |.(w1 - w2).| = 0 implies w1 = w2 )
assume  |.(w1 - w2).| = 0 ; ::_thesis: w1 = w2
then  w1 - w2 = 0. (TOP-REAL N) by Th24;
hence  w1 = w2 by EUCLID:43; ::_thesis: verum
end;

Lm2:  for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st w1 = w2 holds
|.(w1 - w2).| = 0
let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( w1 = w2 implies |.(w1 - w2).| = 0 )
assume  w1 = w2 ; ::_thesis: |.(w1 - w2).| = 0
then |.(w1 - w2).| = |.(0. (TOP-REAL N)).| by EUCLID:42
.= 0 by Th23 ;
hence  |.(w1 - w2).| = 0 ; ::_thesis: verum
end;

theorem :: TOPRNS_1:28
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds
( |.(w1 - w2).| = 0 iff w1 = w2 ) by Lm1, Lm2;

theorem Th29: :: TOPRNS_1:29
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.|
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 + w2).| <= |.w1.| + |.w2.|
let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 + w2).| <= |.w1.| + |.w2.|
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
 w1 + w2 = s1 + s2 ;
hence  |.(w1 + w2).| <= |.w1.| + |.w2.| by EUCLID:12; ::_thesis: verum
end;

theorem :: TOPRNS_1:30
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.w1.| + |.w2.|
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.w1.| + |.w2.|
let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| <= |.w1.| + |.w2.|
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
 w1 - w2 = s1 - s2 ;
hence  |.(w1 - w2).| <= |.w1.| + |.w2.| by EUCLID:13; ::_thesis: verum
end;

theorem :: TOPRNS_1:31
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 + w2).|
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 + w2).|
let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.w1.| - |.w2.| <= |.(w1 + w2).|
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
 w1 + w2 = s1 + s2 ;
hence  |.w1.| - |.w2.| <= |.(w1 + w2).| by EUCLID:14; ::_thesis: verum
end;

theorem Th32: :: TOPRNS_1:32
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).|
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) holds |.w1.| - |.w2.| <= |.(w1 - w2).|
let w1, w2 be Point of (TOP-REAL N); ::_thesis: |.w1.| - |.w2.| <= |.(w1 - w2).|
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
 w1 - w2 = s1 - s2 ;
hence  |.w1.| - |.w2.| <= |.(w1 - w2).| by EUCLID:15; ::_thesis: verum
end;

theorem :: TOPRNS_1:33
for N being Element of NAT
for w1, w2 being Point of (TOP-REAL N) st w1 <> w2 holds
|.(w1 - w2).| > 0
proof
let N be Element of NAT ; ::_thesis: for w1, w2 being Point of (TOP-REAL N) st w1 <> w2 holds
|.(w1 - w2).| > 0
let w1, w2 be Point of (TOP-REAL N); ::_thesis: ( w1 <> w2 implies |.(w1 - w2).| > 0 )
reconsider s1 = w1, s2 = w2 as Element of REAL N by EUCLID:22;
 s1 - s2 = w1 - w2 ;
hence  ( w1 <> w2 implies |.(w1 - w2).| > 0 ) by EUCLID:17; ::_thesis: verum
end;

theorem :: TOPRNS_1:34
for N being Element of NAT
for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
proof
let N be Element of NAT ; ::_thesis: for w1, w2, w being Point of (TOP-REAL N) holds |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
let w1, w2, w be Point of (TOP-REAL N); ::_thesis: |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).|
0. (TOP-REAL N) = w - w by EUCLID:42
.= (- w) + w by EUCLID:41 ;
then |.(w1 - w2).| = |.((w1 + ((- w) + w)) - w2).| by EUCLID:27
.= |.(((w1 + (- w)) + w) - w2).| by EUCLID:26
.= |.(((w1 - w) + w) - w2).| by EUCLID:41
.= |.((w1 - w) + (w - w2)).| by EUCLID:45 ;
hence  |.(w1 - w2).| <= |.(w1 - w).| + |.(w - w2).| by Th29; ::_thesis: verum
end;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is bounded  means :Def7: :: TOPRNS_1:def 7
 ex r being Real st
for n being Element of NAT holds |.(IT . n).| < r;
end;

:: deftheorem Def7 defines bounded TOPRNS_1:def_7_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is bounded iff ex r being Real st
for n being Element of NAT holds |.(IT . n).| < r );

theorem Th35: :: TOPRNS_1:35
for N being Element of NAT
for seq being Real_Sequence of N
for n being Element of NAT ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(seq . m).| < r ) )
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N
for n being Element of NAT ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(seq . m).| < r ) )
let seq be Real_Sequence of N; ::_thesis: for n being Element of NAT ex r being Real st
( 0 < r & ( for m being Element of NAT st m <= n holds
|.(seq . m).| < r ) )
defpred S1[ Element of NAT ] means  ex r1 being Real st
( 0 < r1 & ( for m being Element of NAT st m <= $1 holds
|.(seq . m).| < r1 ) );
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
given r1 being Real such that A2: 0 < r1 and
A3: for m being Element of NAT st m <= n holds
|.(seq . m).| < r1 ; ::_thesis: S1[n + 1]
A4: now__::_thesis:_(_r1_<=_|.(seq_._(n_+_1)).|_implies_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
|.(seq_._m).|_<_r_)_)_)
assume A5: r1 <= |.(seq . (n + 1)).| ; ::_thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = |.(seq . (n + 1)).| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r ) )
thus  0 < r ; ::_thesis: for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A6: m <= n + 1 ; ::_thesis: |.(seq . m).| < r
A7: now__::_thesis:_(_m_<=_n_implies_|.(seq_._m).|_<_r_)
assume  m <= n ; ::_thesis: |.(seq . m).| < r
then  |.(seq . m).| < r1 by A3;
then  |.(seq . m).| < |.(seq . (n + 1)).| by A5, XXREAL_0:2;
then  |.(seq . m).| + 0 < r by XREAL_1:8;
hence  |.(seq . m).| < r ; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_|.(seq_._m).|_<_r_)
assume  m = n + 1 ; ::_thesis: |.(seq . m).| < r
then  |.(seq . m).| + 0 < r by XREAL_1:8;
hence  |.(seq . m).| < r ; ::_thesis: verum
end;
hence  |.(seq . m).| < r by A6, A7, NAT_1:8; ::_thesis: verum
end;
now__::_thesis:_(_|.(seq_._(n_+_1)).|_<=_r1_implies_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_
|.(seq_._m).|_<_r_)_)_)
assume A8: |.(seq . (n + 1)).| <= r1 ; ::_thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = r1 + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r ) )
thus  0 < r by A2; ::_thesis: for m being Element of NAT st m <= n + 1 holds
|.(seq . m).| < r
let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A9: m <= n + 1 ; ::_thesis: |.(seq . m).| < r
A10: now__::_thesis:_(_m_<=_n_implies_|.(seq_._m).|_<_r_)
assume  m <= n ; ::_thesis: |.(seq . m).| < r
then A11: |.(seq . m).| < r1 by A3;
 r1 + 0 < r by XREAL_1:8;
hence  |.(seq . m).| < r by A11, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_m_=_n_+_1_implies_|.(seq_._m).|_<_r_)
A12: r1 + 0 < r by XREAL_1:8;
assume  m = n + 1 ; ::_thesis: |.(seq . m).| < r
hence  |.(seq . m).| < r by A8, A12, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(seq . m).| < r by A9, A10, NAT_1:8; ::_thesis: verum
end;
hence  S1[n + 1] by A4; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
take r = |.(seq . 0).| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st m <= 0 holds
|.(seq . m).| < r ) )
thus  0 < r ; ::_thesis: for m being Element of NAT st m <= 0 holds
|.(seq . m).| < r
let m be Element of NAT ; ::_thesis: ( m <= 0 implies |.(seq . m).| < r )
assume  m <= 0 ; ::_thesis: |.(seq . m).| < r
then  0 = m ;
then  |.(seq . m).| + 0 < r by XREAL_1:8;
hence  |.(seq . m).| < r ; ::_thesis: verum
end;
thus  for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1); ::_thesis: verum
end;

definition
let N be Element of NAT ;
let IT be Real_Sequence of N;
attrIT is convergent  means :Def8: :: TOPRNS_1:def 8
 ex g being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((IT . m) - g).| < r;
end;

:: deftheorem Def8 defines convergent TOPRNS_1:def_8_:_
 for N being Element of NAT
for IT being Real_Sequence of N holds
( IT is convergent iff ex g being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((IT . m) - g).| < r );

definition
let N be Element of NAT ;
let seq be Real_Sequence of N;
assume A1: seq is convergent ;
func lim seq ->  Point of (TOP-REAL N) means :Def9: :: TOPRNS_1:def 9
 for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - it).| < r;
existence
 ex b1 being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b1).| < r by A1, Def8;
uniqueness
 for b1, b2 being Point of (TOP-REAL N) st ( for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b1).| < r ) & ( for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b2).| < r ) holds
b1 = b2
proof
given g1, g2 being Point of (TOP-REAL N) such that A2: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < r and
A3: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g2).| < r and
A4: g1 <> g2 ; ::_thesis: contradiction
A5: now__::_thesis:_not_|.(g1_-_g2).|_=_0
assume  |.(g1 - g2).| = 0 ; ::_thesis: contradiction
then  (0. (TOP-REAL N)) + g2 = (g1 - g2) + g2 by Th24;
then g2 = (g1 - g2) + g2 by EUCLID:27
.= g1 - (g2 - g2) by EUCLID:47
.= g1 - (0. (TOP-REAL N)) by EUCLID:42
.= g1 + (- (0. (TOP-REAL N))) by EUCLID:41
.= g1 + ((- 1) * (0. (TOP-REAL N))) by EUCLID:39
.= g1 + (0. (TOP-REAL N)) by EUCLID:28
.= g1 by EUCLID:27 ;
hence  contradiction by A4; ::_thesis: verum
end;
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < |.(g1 - g2).| / 4 by A2, XREAL_1:224;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
|.((seq . m) - g2).| < |.(g1 - g2).| / 4 by A3, A5, XREAL_1:224;
A8: |.((seq . (n1 + n2)) - g2).| < |.(g1 - g2).| / 4 by A7, NAT_1:12;
 |.((seq . (n1 + n2)) - g1).| < |.(g1 - g2).| / 4 by A6, NAT_1:12;
then A9: |.((seq . (n1 + n2)) - g2).| + |.((seq . (n1 + n2)) - g1).| < (|.(g1 - g2).| / 4) + (|.(g1 - g2).| / 4) by A8, XREAL_1:8;
|.(g1 - g2).| = |.((g1 - g2) + (0. (TOP-REAL N))).| by EUCLID:27
.= |.((g1 - g2) + ((- 1) * (0. (TOP-REAL N)))).| by EUCLID:28
.= |.((g1 - g2) + (- (0. (TOP-REAL N)))).| by EUCLID:39
.= |.((g1 - g2) - (0. (TOP-REAL N))).| by EUCLID:41
.= |.((g1 - g2) - ((seq . (n1 + n2)) - (seq . (n1 + n2)))).| by EUCLID:42
.= |.(((g1 - g2) - (seq . (n1 + n2))) + (seq . (n1 + n2))).| by EUCLID:47
.= |.((g1 - ((seq . (n1 + n2)) + g2)) + (seq . (n1 + n2))).| by EUCLID:46
.= |.(((g1 - (seq . (n1 + n2))) - g2) + (seq . (n1 + n2))).| by EUCLID:46
.= |.((g1 - (seq . (n1 + n2))) - (g2 - (seq . (n1 + n2)))).| by EUCLID:47
.= |.((g1 - (seq . (n1 + n2))) + (- (g2 - (seq . (n1 + n2))))).| by EUCLID:41
.= |.((g1 - (seq . (n1 + n2))) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44
.= |.((- ((seq . (n1 + n2)) - g1)) + ((seq . (n1 + n2)) - g2)).| by EUCLID:44 ;
then  |.(g1 - g2).| <= |.(- ((seq . (n1 + n2)) - g1)).| + |.((seq . (n1 + n2)) - g2).| by Th29;
then A10: |.(g1 - g2).| <= |.((seq . (n1 + n2)) - g1).| + |.((seq . (n1 + n2)) - g2).| by EUCLID:71;
 |.(g1 - g2).| / 2 < |.(g1 - g2).| by A5, XREAL_1:216;
hence  contradiction by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines lim TOPRNS_1:def_9_:_
 for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
for b3 being Point of (TOP-REAL N) holds
( b3 = lim seq iff for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - b3).| < r );

theorem Th36: :: TOPRNS_1:36
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq + seq9 is convergent
proof
let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq + seq9 is convergent
let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies seq + seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: seq + seq9 is convergent
consider g1 being Point of (TOP-REAL N) such that
A3: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < r by A1, Def8;
consider g2 being Point of (TOP-REAL N) such that
A4: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq9 . m) - g2).| < r by A2, Def8;
take g = g1 + g2; :: according to TOPRNS_1:def_8 ::_thesis: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq9) . m) - g).| < r
let r be Real; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq9) . m) - g).| < r )
assume A5: 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((seq + seq9) . m) - g).| < r
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < r / 2 by A3, XREAL_1:215;
consider n2 being Element of NAT  such that
A7: for m being Element of NAT st n2 <= m holds
|.((seq9 . m) - g2).| < r / 2 by A4, A5, XREAL_1:215;
take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds
|.(((seq + seq9) . m) - g).| < r
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((seq + seq9) . m) - g).| < r )
assume A8: k <= m ; ::_thesis: |.(((seq + seq9) . m) - g).| < r
 n2 <= k by NAT_1:12;
then  n2 <= m by A8, XXREAL_0:2;
then A9: |.((seq9 . m) - g2).| < r / 2 by A7;
A10: |.(((seq + seq9) . m) - g).| = |.(((seq . m) + (seq9 . m)) - (g1 + g2)).| by Th4
.= |.((seq . m) + ((seq9 . m) - (g1 + g2))).| by EUCLID:45
.= |.((seq . m) + ((- (g1 + g2)) + (seq9 . m))).| by EUCLID:41
.= |.(((seq . m) + (- (g1 + g2))) + (seq9 . m)).| by EUCLID:26
.= |.(((seq . m) - (g1 + g2)) + (seq9 . m)).| by EUCLID:41
.= |.((((seq . m) - g1) - g2) + (seq9 . m)).| by EUCLID:46
.= |.((((seq . m) - g1) + (- g2)) + (seq9 . m)).| by EUCLID:41
.= |.(((seq . m) - g1) + ((seq9 . m) + (- g2))).| by EUCLID:26
.= |.(((seq . m) - g1) + ((seq9 . m) - g2)).| by EUCLID:41 ;
A11: |.(((seq . m) - g1) + ((seq9 . m) - g2)).| <= |.((seq . m) - g1).| + |.((seq9 . m) - g2).| by Th29;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A8, XXREAL_0:2;
then  |.((seq . m) - g1).| < r / 2 by A6;
then  |.((seq . m) - g1).| + |.((seq9 . m) - g2).| < (r / 2) + (r / 2) by A9, XREAL_1:8;
hence  |.(((seq + seq9) . m) - g).| < r by A10, A11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th37: :: TOPRNS_1:37
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
proof
let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
lim (seq + seq9) = (lim seq) + (lim seq9)
let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq + seq9) = (lim seq) + (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: lim (seq + seq9) = (lim seq) + (lim seq9)
A3: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((seq_+_seq9)_._m)_-_((lim_seq)_+_(lim_seq9))).|_<_r
let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r )
assume  0 < r ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
then A4: 0 < r / 2 by XREAL_1:215;
then consider n1 being Element of NAT  such that
A5: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < r / 2 by A1, Def9;
consider n2 being Element of NAT  such that
A6: for m being Element of NAT st n2 <= m holds
|.((seq9 . m) - (lim seq9)).| < r / 2 by A2, A4, Def9;
take k = n1 + n2; ::_thesis: for m being Element of NAT st k <= m holds
|.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r )
assume A7: k <= m ; ::_thesis: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r
 n2 <= k by NAT_1:12;
then  n2 <= m by A7, XXREAL_0:2;
then A8: |.((seq9 . m) - (lim seq9)).| < r / 2 by A6;
A9: |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| = |.((((seq + seq9) . m) - (lim seq)) - (lim seq9)).| by EUCLID:46
.= |.((((seq . m) + (seq9 . m)) - (lim seq)) - (lim seq9)).| by Th4
.= |.(((seq . m) + ((seq9 . m) - (lim seq))) - (lim seq9)).| by EUCLID:45
.= |.(((seq . m) + ((- (lim seq)) + (seq9 . m))) - (lim seq9)).| by EUCLID:41
.= |.((((seq . m) + (- (lim seq))) + (seq9 . m)) - (lim seq9)).| by EUCLID:26
.= |.((((seq . m) - (lim seq)) + (seq9 . m)) - (lim seq9)).| by EUCLID:41
.= |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| by EUCLID:45 ;
A10: |.(((seq . m) - (lim seq)) + ((seq9 . m) - (lim seq9))).| <= |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| by Th29;
 n1 <= n1 + n2 by NAT_1:12;
then  n1 <= m by A7, XXREAL_0:2;
then  |.((seq . m) - (lim seq)).| < r / 2 by A5;
then  |.((seq . m) - (lim seq)).| + |.((seq9 . m) - (lim seq9)).| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence  |.(((seq + seq9) . m) - ((lim seq) + (lim seq9))).| < r by A9, A10, XXREAL_0:2; ::_thesis: verum
end;
 seq + seq9 is convergent by A1, A2, Th36;
hence  lim (seq + seq9) = (lim seq) + (lim seq9) by A3, Def9; ::_thesis: verum
end;

theorem Th38: :: TOPRNS_1:38
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
let r be Real; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies r * seq is convergent )
assume  seq is convergent ; ::_thesis: r * seq is convergent
then consider g1 being Point of (TOP-REAL N) such that
A1: for q being Real st 0 < q holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < q by Def8;
set g = r * g1;
A2: now__::_thesis:_(_r_<>_0_implies_for_q_being_Real_st_0_<_q_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((r_*_seq)_._m)_-_(r_*_g1)).|_<_q_)
A3: 0 / (abs r) = 0 ;
assume A4: r <> 0 ; ::_thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
then A5: 0 < abs r by COMPLEX1:47;
let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q )
assume  0 < q ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
then consider n1 being Element of NAT  such that
A6: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g1).| < q / (abs r) by A1, A5, A3, XREAL_1:74;
take k = n1; ::_thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * g1)).| < q )
assume  k <= m ; ::_thesis: |.(((r * seq) . m) - (r * g1)).| < q
then A7: |.((seq . m) - g1).| < q / (abs r) by A6;
A8: 0 < abs r by A4, COMPLEX1:47;
A9: (abs r) * (q / (abs r)) = (abs r) * (((abs r) ") * q) by XCMPLX_0:def_9
.= ((abs r) * ((abs r) ")) * q
.= 1 * q by A8, XCMPLX_0:def_7
.= q ;
|.(((r * seq) . m) - (r * g1)).| = |.((r * (seq . m)) - (r * g1)).| by Th5
.= |.(r * ((seq . m) - g1)).| by EUCLID:49
.= (abs r) * |.((seq . m) - g1).| by Th7 ;
hence  |.(((r * seq) . m) - (r * g1)).| < q by A5, A7, A9, XREAL_1:68; ::_thesis: verum
end;
now__::_thesis:_(_r_=_0_implies_for_q_being_Real_st_0_<_q_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((r_*_seq)_._m)_-_(r_*_g1)).|_<_q_)
assume A10: r = 0 ; ::_thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q )
assume A11: 0 < q ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * g1)).| < q )
assume  k <= m ; ::_thesis: |.(((r * seq) . m) - (r * g1)).| < q
|.(((r * seq) . m) - (r * g1)).| = |.(((0 * seq) . m) - (0. (TOP-REAL N))).| by A10, EUCLID:29
.= |.((0. (TOP-REAL N)) - ((0 * seq) . m)).| by Th27
.= |.((0. (TOP-REAL N)) + (- ((0 * seq) . m))).| by EUCLID:41
.= |.(- ((0 * seq) . m)).| by EUCLID:27
.= |.((0 * seq) . m).| by EUCLID:71
.= |.(0 * (seq . m)).| by Th5
.= |.(0. (TOP-REAL N)).| by EUCLID:29
.= 0 by Th23 ;
hence  |.(((r * seq) . m) - (r * g1)).| < q by A11; ::_thesis: verum
end;
hence  r * seq is convergent by A2, Def8; ::_thesis: verum
end;

theorem Th39: :: TOPRNS_1:39
for N being Element of NAT
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
proof
let N be Element of NAT ; ::_thesis: for r being Real
for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
let r be Real; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies lim (r * seq) = r * (lim seq) )
A1: now__::_thesis:_(_r_=_0_implies_for_q_being_Real_st_0_<_q_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((r_*_seq)_._m)_-_(r_*_(lim_seq))).|_<_q_)
assume A2: r = 0 ; ::_thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume A3: 0 < q ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
take k = 0 ; ::_thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q )
assume  k <= m ; ::_thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q
 r * (lim seq) = 0. (TOP-REAL N) by A2, EUCLID:29;
then |.(((r * seq) . m) - (r * (lim seq))).| = |.((0 * (seq . m)) - (0. (TOP-REAL N))).| by A2, Th5
.= |.((0. (TOP-REAL N)) - (0 * (seq . m))).| by Th27
.= |.((0. (TOP-REAL N)) + (- (0 * (seq . m)))).| by EUCLID:41
.= |.(- (0 * (seq . m))).| by EUCLID:27
.= |.(0 * (seq . m)).| by EUCLID:71
.= |.(0. (TOP-REAL N)).| by EUCLID:29
.= 0 by Th23 ;
hence  |.(((r * seq) . m) - (r * (lim seq))).| < q by A3; ::_thesis: verum
end;
assume A4: seq is convergent ; ::_thesis: lim (r * seq) = r * (lim seq)
A5: now__::_thesis:_(_r_<>_0_implies_for_q_being_Real_st_0_<_q_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.(((r_*_seq)_._m)_-_(r_*_(lim_seq))).|_<_q_)
A6: 0 / (abs r) = 0 ;
assume A7: r <> 0 ; ::_thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then A8: 0 < abs r by COMPLEX1:47;
let q be Real; ::_thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume  0 < q ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then  0 < q / (abs r) by A8, A6, XREAL_1:74;
then consider n1 being Element of NAT  such that
A9: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < q / (abs r) by A4, Def9;
take k = n1; ::_thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Element of NAT ; ::_thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q )
assume  k <= m ; ::_thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q
then A10: |.((seq . m) - (lim seq)).| < q / (abs r) by A9;
A11: 0 <> abs r by A7, COMPLEX1:47;
A12: (abs r) * (q / (abs r)) = (abs r) * (((abs r) ") * q) by XCMPLX_0:def_9
.= ((abs r) * ((abs r) ")) * q
.= 1 * q by A11, XCMPLX_0:def_7
.= q ;
|.(((r * seq) . m) - (r * (lim seq))).| = |.((r * (seq . m)) - (r * (lim seq))).| by Th5
.= |.(r * ((seq . m) - (lim seq))).| by EUCLID:49
.= (abs r) * |.((seq . m) - (lim seq)).| by Th7 ;
hence  |.(((r * seq) . m) - (r * (lim seq))).| < q by A8, A10, A12, XREAL_1:68; ::_thesis: verum
end;
 r * seq is convergent by A4, Th38;
hence  lim (r * seq) = r * (lim seq) by A1, A5, Def9; ::_thesis: verum
end;

theorem Th40: :: TOPRNS_1:40
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
- seq is convergent
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds
- seq is convergent
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies - seq is convergent )
assume  seq is convergent ; ::_thesis: - seq is convergent
then  (- 1) * seq is convergent by Th38;
hence  - seq is convergent by Th11; ::_thesis: verum
end;

theorem Th41: :: TOPRNS_1:41
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )
assume  seq is convergent ; ::_thesis: lim (- seq) = - (lim seq)
then  lim ((- 1) * seq) = (- 1) * (lim seq) by Th39
.= - (1 * (lim seq)) by EUCLID:40
.= - (lim seq) by EUCLID:29 ;
hence  lim (- seq) = - (lim seq) by Th11; ::_thesis: verum
end;

theorem :: TOPRNS_1:42
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent
proof
let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
seq - seq9 is convergent
let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies seq - seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: seq - seq9 is convergent
 - seq9 is convergent by A2, Th40;
hence  seq - seq9 is convergent by A1, Th36; ::_thesis: verum
end;

theorem :: TOPRNS_1:43
for N being Element of NAT
for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
lim (seq - seq9) = (lim seq) - (lim seq9)
proof
let N be Element of NAT ; ::_thesis: for seq, seq9 being Real_Sequence of N st seq is convergent & seq9 is convergent holds
lim (seq - seq9) = (lim seq) - (lim seq9)
let seq, seq9 be Real_Sequence of N; ::_thesis: ( seq is convergent & seq9 is convergent implies lim (seq - seq9) = (lim seq) - (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; ::_thesis: lim (seq - seq9) = (lim seq) - (lim seq9)
 - seq9 is convergent by A2, Th40;
hence  lim (seq - seq9) = (lim seq) + (lim (- seq9)) by A1, Th37
.= (lim seq) + (- (lim seq9)) by A2, Th41
.= (lim seq) - (lim seq9) by EUCLID:41 ;
::_thesis: verum
end;

theorem :: TOPRNS_1:44
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent holds
seq is bounded
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent holds
seq is bounded
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent implies seq is bounded )
assume  seq is convergent ; ::_thesis: seq is bounded
then consider g being Point of (TOP-REAL N) such that
A1: for r being Real st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g).| < r by Def8;
consider n1 being Element of NAT  such that
A2: for m being Element of NAT st n1 <= m holds
|.((seq . m) - g).| < 1 by A1;
A3: now__::_thesis:_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_st_n1_<=_m_holds_
|.(seq_._m).|_<_r_)_)
take r = |.g.| + 1; ::_thesis: ( 0 < r & ( for m being Element of NAT st n1 <= m holds
|.(seq . m).| < r ) )
thus  0 < r ; ::_thesis: for m being Element of NAT st n1 <= m holds
|.(seq . m).| < r
let m be Element of NAT ; ::_thesis: ( n1 <= m implies |.(seq . m).| < r )
A4: (|.(seq . m).| - |.g.|) + |.g.| = |.(seq . m).| ;
assume  n1 <= m ; ::_thesis: |.(seq . m).| < r
then A5: |.((seq . m) - g).| < 1 by A2;
 |.(seq . m).| - |.g.| <= |.((seq . m) - g).| by Th32;
then  |.(seq . m).| - |.g.| < 1 by A5, XXREAL_0:2;
hence  |.(seq . m).| < r by A4, XREAL_1:6; ::_thesis: verum
end;
now__::_thesis:_ex_r_being_Element_of_REAL_st_
(_0_<_r_&_(_for_m_being_Element_of_NAT_holds_|.(seq_._m).|_<_r_)_)
consider r2 being Real such that
A6: 0 < r2 and
A7: for m being Element of NAT st m <= n1 holds
|.(seq . m).| < r2 by Th35;
consider r1 being Real such that
A8: 0 < r1 and
A9: for m being Element of NAT st n1 <= m holds
|.(seq . m).| < r1 by A3;
take r = r1 + r2; ::_thesis: ( 0 < r & ( for m being Element of NAT holds |.(seq . m).| < r ) )
thus  0 < r by A8, A6; ::_thesis: for m being Element of NAT holds |.(seq . m).| < r
let m be Element of NAT ; ::_thesis: |.(seq . m).| < r
A10: 0 + r2 < r by A8, XREAL_1:8;
A11: now__::_thesis:_(_m_<=_n1_implies_|.(seq_._m).|_<_r_)
assume  m <= n1 ; ::_thesis: |.(seq . m).| < r
then  |.(seq . m).| < r2 by A7;
hence  |.(seq . m).| < r by A10, XXREAL_0:2; ::_thesis: verum
end;
A12: r1 + 0 < r by A6, XREAL_1:8;
now__::_thesis:_(_n1_<=_m_implies_|.(seq_._m).|_<_r_)
assume  n1 <= m ; ::_thesis: |.(seq . m).| < r
then  |.(seq . m).| < r1 by A9;
hence  |.(seq . m).| < r by A12, XXREAL_0:2; ::_thesis: verum
end;
hence  |.(seq . m).| < r by A11; ::_thesis: verum
end;
hence  seq is bounded by Def7; ::_thesis: verum
end;

theorem :: TOPRNS_1:45
for N being Element of NAT
for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
proof
let N be Element of NAT ; ::_thesis: for seq being Real_Sequence of N st seq is convergent & lim seq <> 0. (TOP-REAL N) holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
let seq be Real_Sequence of N; ::_thesis: ( seq is convergent & lim seq <> 0. (TOP-REAL N) implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).| )
assume that
A1: seq is convergent and
A2: lim seq <> 0. (TOP-REAL N) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
 0 <> |.(lim seq).| by A2, Th24;
then  0 < |.(lim seq).| / 2 by XREAL_1:215;
then consider n1 being Element of NAT  such that
A3: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A1, Def9;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
|.(lim seq).| / 2 < |.(seq . m).|
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(lim seq).| / 2 < |.(seq . m).| )
assume  n <= m ; ::_thesis: |.(lim seq).| / 2 < |.(seq . m).|
then A4: |.((seq . m) - (lim seq)).| < |.(lim seq).| / 2 by A3;
 ( |.(lim seq).| - |.(seq . m).| <= |.((lim seq) - (seq . m)).| & |.((lim seq) - (seq . m)).| = |.((seq . m) - (lim seq)).| ) by Th27, Th32;
then A5: |.(lim seq).| - |.(seq . m).| < |.(lim seq).| / 2 by A4, XXREAL_0:2;
 ( (|.(lim seq).| / 2) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(seq . m).| & (|.(lim seq).| - |.(seq . m).|) + (|.(seq . m).| - (|.(lim seq).| / 2)) = |.(lim seq).| / 2 ) ;
hence  |.(lim seq).| / 2 < |.(seq . m).| by A5, XREAL_1:6; ::_thesis: verum
end;