:: SEQM_3 semantic presentation

Lemma1: for b₁, b₂ being Nat st b₁ < b₂ holds
ex b₃ being Nat st b₂ = (b₁ + 1) + b₃

proof end;

Lemma2: for b₁ being Real_Sequence holds
( ( ( for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) ) implies for b₂, b₃ being Nat holds b₁ . b₂ < b₁ . ((b₂ + 1) + b₃) ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ < b₁ . ((b₂ + 1) + b₃) ) implies for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₂ < b₁ . b₃ ) & ( ( for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₂ < b₁ . b₃ ) implies for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) ) )

proof end;

Lemma3: for b₁ being Real_Sequence holds
( ( ( for b₂ being Nat holds b₁ . (b₂ + 1) < b₁ . b₂ ) implies for b₂, b₃ being Nat holds b₁ . ((b₂ + 1) + b₃) < b₁ . b₂ ) & ( ( for b₂, b₃ being Nat holds b₁ . ((b₂ + 1) + b₃) < b₁ . b₂ ) implies for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₃ < b₁ . b₂ ) & ( ( for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₃ < b₁ . b₂ ) implies for b₂ being Nat holds b₁ . (b₂ + 1) < b₁ . b₂ ) )

proof end;

Lemma4: for b₁ being Real_Sequence holds
( ( ( for b₂ being Nat holds b₁ . b₂ <= b₁ . (b₂ + 1) ) implies for b₂, b₃ being Nat holds b₁ . b₂ <= b₁ . (b₂ + b₃) ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ <= b₁ . (b₂ + b₃) ) implies for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃ ) & ( ( for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃ ) implies for b₂ being Nat holds b₁ . b₂ <= b₁ . (b₂ + 1) ) )

proof end;

Lemma5: for b₁ being Real_Sequence holds
( ( ( for b₂ being Nat holds b₁ . (b₂ + 1) <= b₁ . b₂ ) implies for b₂, b₃ being Nat holds b₁ . (b₂ + b₃) <= b₁ . b₂ ) & ( ( for b₂, b₃ being Nat holds b₁ . (b₂ + b₃) <= b₁ . b₂ ) implies for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ <= b₁ . b₂ ) & ( ( for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ <= b₁ . b₂ ) implies for b₂ being Nat holds b₁ . (b₂ + 1) <= b₁ . b₂ ) )

proof end;

definition

let c₁ be PartFunc of NAT , REAL ;
attr a₁ is increasing means :Def1: :: SEQM_3:def 1
for b₁, b₂ being Nat st b₁ in dom a₁ & b₂ in dom a₁ & b₁ < b₂ holds
a₁ . b₁ < a₁ . b₂;
attr a₁ is decreasing means :Def2: :: SEQM_3:def 2
for b₁, b₂ being Nat st b₁ in dom a₁ & b₂ in dom a₁ & b₁ < b₂ holds
a₁ . b₁ > a₁ . b₂;
attr a₁ is non-decreasing means :Def3: :: SEQM_3:def 3
for b₁, b₂ being Nat st b₁ in dom a₁ & b₂ in dom a₁ & b₁ <= b₂ holds
a₁ . b₁ <= a₁ . b₂;
attr a₁ is non-increasing means :Def4: :: SEQM_3:def 4
for b₁, b₂ being Nat st b₁ in dom a₁ & b₂ in dom a₁ & b₁ <= b₂ holds
a₁ . b₁ >= a₁ . b₂;

end;

:: deftheorem Def1 defines increasing SEQM_3:def 1 :

:: deftheorem Def2 defines decreasing SEQM_3:def 2 :

:: deftheorem Def3 defines non-decreasing SEQM_3:def 3 :

:: deftheorem Def4 defines non-increasing SEQM_3:def 4 :

Lemma10: for b₁ being Real_Sequence holds
( b₁ is increasing iff for b₂ being Nat holds b₁ . b₂ < b₁ . (b₂ + 1) )

proof end;

Lemma11: for b₁ being Real_Sequence holds
( b₁ is decreasing iff for b₂ being Nat holds b₁ . b₂ > b₁ . (b₂ + 1) )

proof end;

Lemma12: for b₁ being Real_Sequence holds
( b₁ is non-decreasing iff for b₂ being Nat holds b₁ . b₂ <= b₁ . (b₂ + 1) )

proof end;

Lemma13: for b₁ being Real_Sequence holds
( b₁ is non-increasing iff for b₂ being Nat holds b₁ . b₂ >= b₁ . (b₂ + 1) )

proof end;

definition

let c₁ be Function;
attr a₁ is constant means :Def5: :: SEQM_3:def 5
for b₁, b₂ being set st b₁ in dom a₁ & b₂ in dom a₁ holds
a₁ . b₁ = a₁ . b₂;

end;

:: deftheorem Def5 defines constant SEQM_3:def 5 :

definition

let c₁ be Real_Sequence;
redefine attr a₁ is constant means :Def6: :: SEQM_3:def 6
ex b₁ being real number st
for b₂ being Nat holds a₁ . b₂ = b₁;
compatibility

proof end;

end;

:: deftheorem Def6 defines constant SEQM_3:def 6 :

definition

let c₁ be Real_Sequence;
attr a₁ is monotone means :Def7: :: SEQM_3:def 7
( a₁ is non-decreasing or a₁ is non-increasing );

end;

:: deftheorem Def7 defines monotone SEQM_3:def 7 :

theorem Th1: :: SEQM_3:1

canceled;

theorem Th2: :: SEQM_3:2

canceled;

theorem Th3: :: SEQM_3:3

canceled;

theorem Th4: :: SEQM_3:4

canceled;

theorem Th5: :: SEQM_3:5

canceled;

theorem Th6: :: SEQM_3:6

canceled;

theorem Th7: :: SEQM_3:7

for b₁ being Real_Sequence holds
( b₁ is increasing iff for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₂ < b₁ . b₃ )

proof end;

theorem Th8: :: SEQM_3:8

for b₁ being Real_Sequence holds
( b₁ is increasing iff for b₂, b₃ being Nat holds b₁ . b₂ < b₁ . ((b₂ + 1) + b₃) )

proof end;

theorem Th9: :: SEQM_3:9

for b₁ being Real_Sequence holds
( b₁ is decreasing iff for b₂, b₃ being Nat holds b₁ . ((b₂ + 1) + b₃) < b₁ . b₂ )

proof end;

theorem Th10: :: SEQM_3:10

for b₁ being Real_Sequence holds
( b₁ is decreasing iff for b₂, b₃ being Nat st b₂ < b₃ holds
b₁ . b₃ < b₁ . b₂ )

proof end;

theorem Th11: :: SEQM_3:11

for b₁ being Real_Sequence holds
( b₁ is non-decreasing iff for b₂, b₃ being Nat holds b₁ . b₂ <= b₁ . (b₂ + b₃) )

proof end;

theorem Th12: :: SEQM_3:12

for b₁ being Real_Sequence holds
( b₁ is non-decreasing iff for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃ )

proof end;

theorem Th13: :: SEQM_3:13

for b₁ being Real_Sequence holds
( b₁ is non-increasing iff for b₂, b₃ being Nat holds b₁ . (b₂ + b₃) <= b₁ . b₂ )

proof end;

theorem Th14: :: SEQM_3:14

for b₁ being Real_Sequence holds
( b₁ is non-increasing iff for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₃ <= b₁ . b₂ )

proof end;

Lemma24: for b₁ being Real_Sequence holds
( ( ex b₂ being real number st
for b₃ being Nat holds b₁ . b₃ = b₂ implies ex b₂ being real number st rng b₁ = {b₂} ) & ( ex b₂ being real number st rng b₁ = {b₂} implies for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) ) & ( ( for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) ) implies for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) ) implies for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ ) & ( ( for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ ) implies ex b₂ being real number st
for b₃ being Nat holds b₁ . b₃ = b₂ ) )

proof end;

theorem Th15: :: SEQM_3:15

for b₁ being Real_Sequence holds
( b₁ is constant iff ex b₂ being real number st rng b₁ = {b₂} )

proof end;

theorem Th16: :: SEQM_3:16

for b₁ being Real_Sequence holds
( b₁ is constant iff for b₂ being Nat holds b₁ . b₂ = b₁ . (b₂ + 1) )

proof end;

theorem Th17: :: SEQM_3:17

for b₁ being Real_Sequence holds
( b₁ is constant iff for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . (b₂ + b₃) )

proof end;

theorem Th18: :: SEQM_3:18

for b₁ being Real_Sequence holds
( b₁ is constant iff for b₂, b₃ being Nat holds b₁ . b₂ = b₁ . b₃ )

proof end;

theorem Th19: :: SEQM_3:19

for b₁ being Real_Sequence st b₁ is increasing holds
for b₂ being Nat st 0 < b₂ holds
b₁ . 0 < b₁ . b₂ by Th7;

theorem Th20: :: SEQM_3:20

for b₁ being Real_Sequence st b₁ is decreasing holds
for b₂ being Nat st 0 < b₂ holds
b₁ . b₂ < b₁ . 0 by Th10;

theorem Th21: :: SEQM_3:21

for b₁ being Real_Sequence st b₁ is non-decreasing holds
for b₂ being Nat holds b₁ . 0 <= b₁ . b₂

proof end;

theorem Th22: :: SEQM_3:22

for b₁ being Real_Sequence st b₁ is non-increasing holds
for b₂ being Nat holds b₁ . b₂ <= b₁ . 0

proof end;

registration

cluster increasing -> non-decreasing M5( NAT , REAL );
coherence

proof end;

cluster decreasing -> non-increasing M5( NAT , REAL );
coherence

proof end;

cluster constant -> non-decreasing non-increasing M5( NAT , REAL );
coherence

proof end;

cluster non-decreasing non-increasing -> constant M5( NAT , REAL );
coherence

proof end;

end;

theorem Th23: :: SEQM_3:23

for b₁ being Real_Sequence st b₁ is increasing holds
b₁ is non-decreasing

proof end;

theorem Th24: :: SEQM_3:24

for b₁ being Real_Sequence st b₁ is decreasing holds
b₁ is non-increasing

proof end;

theorem Th25: :: SEQM_3:25

for b₁ being Real_Sequence st b₁ is constant holds
b₁ is non-decreasing

proof end;

theorem Th26: :: SEQM_3:26

for b₁ being Real_Sequence st b₁ is constant holds
b₁ is non-increasing

proof end;

theorem Th27: :: SEQM_3:27

for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is non-increasing holds
b₁ is constant

proof end;

definition

let c₁ be Relation;
attr a₁ is natural-yielding means :Def8: :: SEQM_3:def 8
rng a₁ c= NAT ;

end;

:: deftheorem Def8 defines natural-yielding SEQM_3:def 8 :

Lemma34: ( incl NAT is increasing & incl NAT is natural-yielding )

proof end;

registration

cluster increasing non-decreasing natural-yielding M5( NAT , REAL );
existence by Lemma34;

end;

definition

mode Seq_of_Nat is natural-yielding Real_Sequence;

end;

definition

let c₁ be Real_Sequence;
let c₂ be Nat;
func c₁ ^\ c₂ -> Real_Sequence means :Def9: :: SEQM_3:def 9
for b₁ being Nat holds a₃ . b₁ = a₁ . (b₁ + a₂);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines ^\ SEQM_3:def 9 :

theorem Th28: :: SEQM_3:28

canceled;

theorem Th29: :: SEQM_3:29

for b₁ being Real_Sequence holds
( b₁ is increasing Seq_of_Nat iff ( b₁ is increasing & ( for b₂ being Nat holds b₁ . b₂ is Nat ) ) )

proof end;

theorem Th30: :: SEQM_3:30

canceled;

theorem Th31: :: SEQM_3:31

for b₁ being Real_Sequence
for b₂ being increasing Seq_of_Nat
for b₃ being Nat holds (b₁ * b₂) . b₃ = b₁ . (b₂ . b₃)

proof end;

definition

let c₁ be increasing Seq_of_Nat;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Nat;
coherence by Th29;

end;

definition

let c₁ be increasing Seq_of_Nat;
let c₂ be Real_Sequence;
redefine func * as c₂ * c₁ -> Real_Sequence;
coherence

proof end;

end;

definition

let c₁, c₂ be increasing Seq_of_Nat;
redefine func * as c₂ * c₁ -> increasing Seq_of_Nat;
coherence

proof end;

end;

registration

let c₁ be increasing Seq_of_Nat;
let c₂ be Nat;
cluster a₁ ^\ a₂ -> increasing non-decreasing natural-yielding ;
coherence

proof end;

end;

definition

let c₁ be Real_Sequence;
mode subsequence of c₁ -> Real_Sequence means :Def10: :: SEQM_3:def 10
ex b₁ being increasing Seq_of_Nat st a₂ = a₁ * b₁;
existence

proof end;

end;

:: deftheorem Def10 defines subsequence SEQM_3:def 10 :

definition

let c₁ be Real_Sequence;
redefine attr a₁ is increasing means :: SEQM_3:def 11
for b₁ being Nat holds a₁ . b₁ < a₁ . (b₁ + 1);
compatibility by Lemma10;
redefine attr a₁ is decreasing means :: SEQM_3:def 12
for b₁ being Nat holds a₁ . b₁ > a₁ . (b₁ + 1);
compatibility by Lemma11;
redefine attr a₁ is non-decreasing means :: SEQM_3:def 13
for b₁ being Nat holds a₁ . b₁ <= a₁ . (b₁ + 1);
compatibility by Lemma12;
redefine attr a₁ is non-increasing means :: SEQM_3:def 14
for b₁ being Nat holds a₁ . b₁ >= a₁ . (b₁ + 1);
compatibility by Lemma13;

end;

:: deftheorem Def11 defines increasing SEQM_3:def 11 :

:: deftheorem Def12 defines decreasing SEQM_3:def 12 :

:: deftheorem Def13 defines non-decreasing SEQM_3:def 13 :

:: deftheorem Def14 defines non-increasing SEQM_3:def 14 :

theorem Th32: :: SEQM_3:32

canceled;

theorem Th33: :: SEQM_3:33

for b₁ being increasing Seq_of_Nat
for b₂ being Nat holds b₂ <= b₁ . b₂

proof end;

theorem Th34: :: SEQM_3:34

for b₁ being Real_Sequence holds b₁ ^\ 0 = b₁

proof end;

theorem Th35: :: SEQM_3:35

for b₁, b₂ being Nat
for b₃ being Real_Sequence holds (b₃ ^\ b₁) ^\ b₂ = (b₃ ^\ b₂) ^\ b₁

proof end;

theorem Th36: :: SEQM_3:36

for b₁, b₂ being Nat
for b₃ being Real_Sequence holds (b₃ ^\ b₁) ^\ b₂ = b₃ ^\ (b₁ + b₂)

proof end;

theorem Th37: :: SEQM_3:37

for b₁ being Nat
for b₂, b₃ being Real_Sequence holds (b₂ + b₃) ^\ b₁ = (b₂ ^\ b₁) + (b₃ ^\ b₁)

proof end;

theorem Th38: :: SEQM_3:38

for b₁ being Nat
for b₂ being Real_Sequence holds (- b₂) ^\ b₁ = - (b₂ ^\ b₁)

proof end;

theorem Th39: :: SEQM_3:39

for b₁ being Nat
for b₂, b₃ being Real_Sequence holds (b₂ - b₃) ^\ b₁ = (b₂ ^\ b₁) - (b₃ ^\ b₁)

proof end;

theorem Th40: :: SEQM_3:40

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is_not_0 holds
b₂ ^\ b₁ is_not_0

proof end;

theorem Th41: :: SEQM_3:41

for b₁ being Nat
for b₂ being Real_Sequence holds (b₂ " ) ^\ b₁ = (b₂ ^\ b₁) "

proof end;

theorem Th42: :: SEQM_3:42

for b₁ being Nat
for b₂, b₃ being Real_Sequence holds (b₂ (#) b₃) ^\ b₁ = (b₂ ^\ b₁) (#) (b₃ ^\ b₁)

proof end;

theorem Th43: :: SEQM_3:43

for b₁ being Nat
for b₂, b₃ being Real_Sequence holds (b₂ /" b₃) ^\ b₁ = (b₂ ^\ b₁) /" (b₃ ^\ b₁)

proof end;

theorem Th44: :: SEQM_3:44

for b₁ being Nat
for b₂ being real number
for b₃ being Real_Sequence holds (b₂ (#) b₃) ^\ b₁ = b₂ (#) (b₃ ^\ b₁)

proof end;

theorem Th45: :: SEQM_3:45

for b₁ being Nat
for b₂ being Real_Sequence
for b₃ being increasing Seq_of_Nat holds (b₂ * b₃) ^\ b₁ = b₂ * (b₃ ^\ b₁)

proof end;

theorem Th46: :: SEQM_3:46

for b₁ being Real_Sequence holds b₁ is subsequence of b₁

proof end;

theorem Th47: :: SEQM_3:47

for b₁ being Nat
for b₂ being Real_Sequence holds b₂ ^\ b₁ is subsequence of b₂

proof end;

theorem Th48: :: SEQM_3:48

for b₁, b₂, b₃ being Real_Sequence st b₁ is subsequence of b₂ & b₂ is subsequence of b₃ holds
b₁ is subsequence of b₃

proof end;

theorem Th49: :: SEQM_3:49

for b₁, b₂ being Real_Sequence st b₁ is increasing & b₂ is subsequence of b₁ holds
b₂ is increasing

proof end;

theorem Th50: :: SEQM_3:50

for b₁, b₂ being Real_Sequence st b₁ is decreasing & b₂ is subsequence of b₁ holds
b₂ is decreasing

proof end;

theorem Th51: :: SEQM_3:51

for b₁, b₂ being Real_Sequence st b₁ is non-decreasing & b₂ is subsequence of b₁ holds
b₂ is non-decreasing

proof end;

theorem Th52: :: SEQM_3:52

for b₁, b₂ being Real_Sequence st b₁ is non-increasing & b₂ is subsequence of b₁ holds
b₂ is non-increasing

proof end;

theorem Th53: :: SEQM_3:53

for b₁, b₂ being Real_Sequence st b₁ is monotone & b₂ is subsequence of b₁ holds
b₂ is monotone

proof end;

theorem Th54: :: SEQM_3:54

for b₁, b₂ being Real_Sequence st b₁ is constant & b₂ is subsequence of b₁ holds
b₂ is constant

proof end;

theorem Th55: :: SEQM_3:55

for b₁, b₂ being Real_Sequence st b₁ is constant & b₂ is subsequence of b₁ holds
b₁ = b₂

proof end;

theorem Th56: :: SEQM_3:56

for b₁, b₂ being Real_Sequence st b₁ is bounded_above & b₂ is subsequence of b₁ holds
b₂ is bounded_above

proof end;

theorem Th57: :: SEQM_3:57

for b₁, b₂ being Real_Sequence st b₁ is bounded_below & b₂ is subsequence of b₁ holds
b₂ is bounded_below

proof end;

theorem Th58: :: SEQM_3:58

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₂ is subsequence of b₁ holds
b₂ is bounded

proof end;

theorem Th59: :: SEQM_3:59

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is increasing & 0 < b₁ implies b₁ (#) b₂ is increasing ) & ( 0 = b₁ implies b₁ (#) b₂ is constant ) & ( b₂ is increasing & b₁ < 0 implies b₁ (#) b₂ is decreasing ) )

proof end;

theorem Th60: :: SEQM_3:60

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is decreasing & 0 < b₁ implies b₁ (#) b₂ is decreasing ) & ( b₂ is decreasing & b₁ < 0 implies b₁ (#) b₂ is increasing ) )

proof end;

theorem Th61: :: SEQM_3:61

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is non-decreasing & 0 <= b₁ implies b₁ (#) b₂ is non-decreasing ) & ( b₂ is non-decreasing & b₁ <= 0 implies b₁ (#) b₂ is non-increasing ) )

proof end;

theorem Th62: :: SEQM_3:62

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is non-increasing & 0 <= b₁ implies b₁ (#) b₂ is non-increasing ) & ( b₂ is non-increasing & b₁ <= 0 implies b₁ (#) b₂ is non-decreasing ) )

proof end;

theorem Th63: :: SEQM_3:63

for b₁, b₂ being Real_Sequence holds
( ( b₁ is increasing & b₂ is increasing implies b₁ + b₂ is increasing ) & ( b₁ is decreasing & b₂ is decreasing implies b₁ + b₂ is decreasing ) & ( b₁ is non-decreasing & b₂ is non-decreasing implies b₁ + b₂ is non-decreasing ) & ( b₁ is non-increasing & b₂ is non-increasing implies b₁ + b₂ is non-increasing ) )

proof end;

theorem Th64: :: SEQM_3:64

for b₁, b₂ being Real_Sequence holds
( ( b₁ is increasing & b₂ is constant implies b₁ + b₂ is increasing ) & ( b₁ is decreasing & b₂ is constant implies b₁ + b₂ is decreasing ) & ( b₁ is non-decreasing & b₂ is constant implies b₁ + b₂ is non-decreasing ) & ( b₁ is non-increasing & b₂ is constant implies b₁ + b₂ is non-increasing ) )

proof end;

theorem Th65: :: SEQM_3:65

for b₁ being Real_Sequence st b₁ is constant holds
( ( for b₂ being real number holds b₂ (#) b₁ is constant ) & - b₁ is constant & abs b₁ is constant )

proof end;

theorem Th66: :: SEQM_3:66

for b₁, b₂ being Real_Sequence st b₁ is constant & b₂ is constant holds
( b₁ (#) b₂ is constant & b₁ + b₂ is constant )

proof end;

theorem Th67: :: SEQM_3:67

for b₁, b₂ being Real_Sequence st b₁ is constant & b₂ is constant holds
b₁ - b₂ is constant

proof end;

theorem Th68: :: SEQM_3:68

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is bounded_above & 0 < b₁ implies b₁ (#) b₂ is bounded_above ) & ( 0 = b₁ implies b₁ (#) b₂ is bounded ) & ( b₂ is bounded_above & b₁ < 0 implies b₁ (#) b₂ is bounded_below ) )

proof end;

theorem Th69: :: SEQM_3:69

for b₁ being real number
for b₂ being Real_Sequence holds
( ( b₂ is bounded_below & 0 < b₁ implies b₁ (#) b₂ is bounded_below ) & ( b₂ is bounded_below & b₁ < 0 implies b₁ (#) b₂ is bounded_above ) )

proof end;

theorem Th70: :: SEQM_3:70

for b₁ being Real_Sequence holds
( ( b₁ is bounded implies for b₂ being real number holds b₂ (#) b₁ is bounded ) & ( b₁ is bounded implies - b₁ is bounded ) & ( b₁ is bounded implies abs b₁ is bounded ) & ( abs b₁ is bounded implies b₁ is bounded ) )

proof end;

theorem Th71: :: SEQM_3:71

for b₁, b₂ being Real_Sequence holds
( ( b₁ is bounded_above & b₂ is bounded_above implies b₁ + b₂ is bounded_above ) & ( b₁ is bounded_below & b₂ is bounded_below implies b₁ + b₂ is bounded_below ) & ( b₁ is bounded & b₂ is bounded implies b₁ + b₂ is bounded ) )

proof end;

theorem Th72: :: SEQM_3:72

for b₁, b₂ being Real_Sequence st b₁ is bounded & b₂ is bounded holds
( b₁ (#) b₂ is bounded & b₁ - b₂ is bounded )

proof end;

theorem Th73: :: SEQM_3:73

for b₁ being Real_Sequence st b₁ is constant holds
b₁ is bounded

proof end;

theorem Th74: :: SEQM_3:74

for b₁ being Real_Sequence st b₁ is constant holds
( ( for b₂ being real number holds b₂ (#) b₁ is bounded ) & - b₁ is bounded & abs b₁ is bounded )

proof end;

theorem Th75: :: SEQM_3:75

for b₁, b₂ being Real_Sequence holds
( ( b₁ is bounded_above & b₂ is constant implies b₁ + b₂ is bounded_above ) & ( b₁ is bounded_below & b₂ is constant implies b₁ + b₂ is bounded_below ) & ( b₁ is bounded & b₂ is constant implies b₁ + b₂ is bounded ) )

proof end;

theorem Th76: :: SEQM_3:76

for b₁, b₂ being Real_Sequence holds
( ( b₁ is bounded_above & b₂ is constant implies b₁ - b₂ is bounded_above ) & ( b₁ is bounded_below & b₂ is constant implies b₁ - b₂ is bounded_below ) & ( b₁ is bounded & b₂ is constant implies ( b₁ - b₂ is bounded & b₂ - b₁ is bounded & b₁ (#) b₂ is bounded ) ) )

proof end;

theorem Th77: :: SEQM_3:77

for b₁, b₂ being Real_Sequence st b₁ is bounded_above & b₂ is non-increasing holds
b₁ + b₂ is bounded_above

proof end;

theorem Th78: :: SEQM_3:78

for b₁, b₂ being Real_Sequence st b₁ is bounded_below & b₂ is non-decreasing holds
b₁ + b₂ is bounded_below

proof end;

theorem Th79: :: SEQM_3:79

for b₁, b₂ being set holds b₁ --> b₂ is constant

proof end;

registration

let c₁, c₂ be set ;
cluster a₁ --> a₂ -> constant ;
coherence by Th79;

end;

theorem Th80: :: SEQM_3:80

( incl NAT is increasing & incl NAT is natural-yielding ) by Lemma34;