:: SEQ_1 semantic presentation

definition

mode Real_Sequence is Function of NAT , REAL ;

end;

theorem :: SEQ_1:1

canceled;

theorem :: SEQ_1:2

canceled;

theorem Th3: :: SEQ_1:3

for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is real ) ) )

proof end;

theorem Th4: :: SEQ_1:4

for f being Function holds
( f is Real_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is real ) ) )

proof end;

definition

let f be Relation;
attr f is real-yielding means :Def1: :: SEQ_1:def 1
rng f c= REAL ;

end;

:: deftheorem Def1 defines real-yielding SEQ_1:def 1 :

registration

let C be set ;
let D be real-membered set ;
cluster -> real-yielding Relation of C,D;
coherence

proof end;

end;

registration

cluster real-yielding set ;
existence

proof end;

end;

registration

let f be real-yielding Function;
let x be set ;
cluster f . x -> real ;
coherence

proof end;

end;

definition

let f be real-yielding Function;
let x be set ;
:: original: .
redefine func f . x -> Real;
coherence by XREAL_0:def 1;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let x be set ;
:: original: .
redefine func f . x -> Real;
coherence by XREAL_0:def 1;

end;

registration

let F be real-yielding Relation;
let X be set ;
cluster F | X -> real-yielding ;
coherence

proof end;

end;

notation

let f be PartFunc of NAT , REAL ;
synonym being_not_0 f for non-empty f;
synonym f is_not_0 for non-empty f;

end;

definition

let f be PartFunc of NAT , REAL ;
redefine attr f is non-empty means :Def2: :: SEQ_1:def 2
rng f c= REAL \ {0};
compatibility

proof end;

end;

:: deftheorem Def2 defines being_not_0 SEQ_1:def 2 :

theorem :: SEQ_1:5

canceled;

theorem Th6: :: SEQ_1:6

for seq being Real_Sequence holds
( seq is being_not_0 iff for x being set st x in NAT holds
seq . x <> 0 )

proof end;

theorem Th7: :: SEQ_1:7

for seq being Real_Sequence holds
( seq is being_not_0 iff for n being Nat holds seq . n <> 0 )

proof end;

theorem :: SEQ_1:8

for seq, seq1 being Real_Sequence st ( for x being set st x in NAT holds
seq . x = seq1 . x ) holds
seq = seq1

proof end;

theorem :: SEQ_1:9

canceled;

theorem :: SEQ_1:10

for r being real number ex seq being Real_Sequence st rng seq = {r}

proof end;

scheme :: SEQ_1:sch 1
ExRealSeq{ F₁( set ) -> real number } :

ex seq being Real_Sequence st
for n being Nat holds seq . n = F₁(n)

proof end;

scheme :: SEQ_1:sch 2
PartFuncExD'{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff ex c being Element of F₂() st P₁[d,c] ) ) & ( for d being Element of F₁() st d in dom f holds
P₁[d,f . d] ) )

proof end;

scheme :: SEQ_1:sch 3
LambdaPFD'{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), P₁[ set ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff P₁[d] ) ) & ( for d being Element of F₁() st d in dom f holds
f . d = F₃(d) ) )

proof end;

scheme :: SEQ_1:sch 4
UnPartFuncD'{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set ) -> set } :

for f, g being PartFunc of F₁(),F₂() st dom f = F₃() & ( for c being Element of F₁() st c in dom f holds
f . c = F₄(c) ) & dom g = F₃() & ( for c being Element of F₁() st c in dom g holds
g . c = F₄(c) ) holds
f = g

proof end;

definition

let f1, f2 be real-yielding Function;
func f1 + f2 -> Function means :Def3: :: SEQ_1:def 3
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) + (f2 . c) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
func f1 - f2 -> Function means :Def4: :: SEQ_1:def 4
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) - (f2 . c) ) );
existence

proof end;

uniqueness

proof end;

func f1 (#) f2 -> Function means :Def5: :: SEQ_1:def 5
( dom it = (dom f1) /\ (dom f2) & ( for c being set st c in dom it holds
it . c = (f1 . c) * (f2 . c) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def3 defines + SEQ_1:def 3 :

:: deftheorem Def4 defines - SEQ_1:def 4 :

:: deftheorem Def5 defines (#) SEQ_1:def 5 :

registration

let f1, f2 be real-yielding Function;
cluster f1 + f2 -> real-yielding ;
coherence

proof end;

cluster f1 - f2 -> real-yielding ;
coherence

proof end;

cluster f1 (#) f2 -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f1, f2 be PartFunc of C,D;
:: original: +
redefine func f1 + f2 -> PartFunc of C, REAL ;
coherence

proof end;

:: original: -
redefine func f1 - f2 -> PartFunc of C, REAL ;
coherence

proof end;

:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C, REAL ;
coherence

proof end;

end;

theorem Th11: :: SEQ_1:11

for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

proof end;

theorem Th12: :: SEQ_1:12

for seq, seq1, seq2 being Real_Sequence holds
( seq = seq1 (#) seq2 iff for n being Nat holds seq . n = (seq1 . n) * (seq2 . n) )

proof end;

definition

let seq1, seq2 be Real_Sequence;
:: original: +
redefine func seq1 + seq2 -> Real_Sequence;
coherence

proof end;

:: original: -
redefine func seq1 - seq2 -> Real_Sequence;
coherence

proof end;

:: original: (#)
redefine func seq1 (#) seq2 -> Real_Sequence;
coherence

proof end;

end;

definition

let f be real-yielding Function;
let r be real number ;
func r (#) f -> Function means :Def6: :: SEQ_1:def 6
( dom it = dom f & ( for c being set st c in dom it holds
it . c = r * (f . c) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines (#) SEQ_1:def 6 :

registration

let r be real number ;
let f be real-yielding Function;
cluster r (#) f -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
let r be real number ;
:: original: (#)
redefine func r (#) f -> PartFunc of C, REAL ;
coherence

proof end;

end;

definition

let seq be Real_Sequence;
let r be real number ;
:: original: (#)
redefine func r (#) seq -> Real_Sequence;
coherence

proof end;

end;

theorem Th13: :: SEQ_1:13

for r being real number
for seq1, seq2 being Real_Sequence holds
( seq1 = r (#) seq2 iff for n being Nat holds seq1 . n = r * (seq2 . n) )

proof end;

definition

let f be real-yielding Function;
func - f -> Function means :Def7: :: SEQ_1:def 7
( dom it = dom f & ( for c being set st c in dom it holds
it . c = - (f . c) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - SEQ_1:def 7 :

registration

let f be real-yielding Function;
cluster - f -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: -
redefine func - f -> PartFunc of C, REAL ;
coherence

proof end;

end;

definition

let seq be Real_Sequence;
:: original: -
redefine func - seq -> Real_Sequence;
coherence

proof end;

end;

theorem Th14: :: SEQ_1:14

for seq1, seq2 being Real_Sequence holds
( seq1 = - seq2 iff for n being Nat holds seq1 . n = - (seq2 . n) )

proof end;

theorem Th15: :: SEQ_1:15

for seq1, seq2 being Real_Sequence holds seq1 - seq2 = seq1 + (- seq2)

proof end;

definition

let seq be Real_Sequence;
func seq " -> Real_Sequence means :Def8: :: SEQ_1:def 8
for n being Nat holds it . n = (seq . n) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines " SEQ_1:def 8 :

definition

let seq1, seq be Real_Sequence;
func seq1 /" seq -> Real_Sequence equals :: SEQ_1:def 9
seq1 (#) (seq " );
correctness ;

end;

:: deftheorem defines /" SEQ_1:def 9 :

definition

let f be real-yielding Function;
func abs f -> Function means :Def10: :: SEQ_1:def 10
( dom it = dom f & ( for c being set st c in dom it holds
it . c = abs (f . c) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines abs SEQ_1:def 10 :

registration

let f be real-yielding Function;
cluster abs f -> real-yielding ;
coherence

proof end;

end;

definition

let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: abs
redefine func abs f -> PartFunc of C, REAL ;
coherence

proof end;

end;

definition

let seq be Real_Sequence;
:: original: abs
redefine func abs seq -> Real_Sequence;
coherence

proof end;

end;

theorem Th16: :: SEQ_1:16

for seq1, seq being Real_Sequence holds
( seq1 = abs seq iff for n being Nat holds seq1 . n = abs (seq . n) )

proof end;

theorem :: SEQ_1:17

canceled;

theorem :: SEQ_1:18

canceled;

theorem :: SEQ_1:19

canceled;

theorem Th20: :: SEQ_1:20

for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)

proof end;

theorem :: SEQ_1:21

canceled;

theorem Th22: :: SEQ_1:22

for seq1, seq2, seq3 being Real_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)

proof end;

theorem Th23: :: SEQ_1:23

for seq1, seq2, seq3 being Real_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:24

for seq3, seq1, seq2 being Real_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th23;

theorem Th25: :: SEQ_1:25

for seq being Real_Sequence holds - seq = (- 1) (#) seq

proof end;

theorem Th26: :: SEQ_1:26

for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

proof end;

theorem Th27: :: SEQ_1:27

for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

proof end;

theorem Th28: :: SEQ_1:28

for seq1, seq2, seq3 being Real_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)

proof end;

theorem :: SEQ_1:29

for seq3, seq1, seq2 being Real_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th28;

theorem Th30: :: SEQ_1:30

for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

proof end;

theorem Th31: :: SEQ_1:31

for r, p being real number
for seq being Real_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)

proof end;

theorem Th32: :: SEQ_1:32

for r being real number
for seq1, seq2 being Real_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

proof end;

theorem Th33: :: SEQ_1:33

for r being real number
for seq1, seq being Real_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq by Th26;

theorem :: SEQ_1:34

for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem Th35: :: SEQ_1:35

for seq being Real_Sequence holds 1 (#) seq = seq

proof end;

theorem Th36: :: SEQ_1:36

for seq being Real_Sequence holds - (- seq) = seq

proof end;

theorem Th37: :: SEQ_1:37

for seq1, seq2 being Real_Sequence holds seq1 - (- seq2) = seq1 + seq2

proof end;

theorem :: SEQ_1:38

for seq1, seq2, seq3 being Real_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

proof end;

theorem :: SEQ_1:39

for seq1, seq2, seq3 being Real_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3

proof end;

theorem :: SEQ_1:40

for seq1, seq2 being Real_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) )

proof end;

theorem Th41: :: SEQ_1:41

for seq being Real_Sequence st seq is being_not_0 holds
seq " is being_not_0

proof end;

theorem Th42: :: SEQ_1:42

for seq being Real_Sequence holds (seq " ) " = seq

proof end;

theorem Th43: :: SEQ_1:43

for seq, seq1 being Real_Sequence holds
( ( seq is being_not_0 & seq1 is being_not_0 ) iff seq (#) seq1 is being_not_0 )

proof end;

theorem Th44: :: SEQ_1:44

for seq, seq1 being Real_Sequence holds (seq " ) (#) (seq1 " ) = (seq (#) seq1) "

proof end;

theorem :: SEQ_1:45

for seq, seq1 being Real_Sequence st seq is being_not_0 holds
(seq1 /" seq) (#) seq = seq1

proof end;

theorem :: SEQ_1:46

for seq', seq, seq1', seq1 being Real_Sequence holds (seq' /" seq) (#) (seq1' /" seq1) = (seq' (#) seq1') /" (seq (#) seq1)

proof end;

theorem :: SEQ_1:47

for seq, seq1 being Real_Sequence st seq is being_not_0 & seq1 is being_not_0 holds
seq /" seq1 is being_not_0

proof end;

theorem Th48: :: SEQ_1:48

for seq, seq1 being Real_Sequence holds (seq /" seq1) " = seq1 /" seq

proof end;

theorem Th49: :: SEQ_1:49

for seq2, seq1, seq being Real_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq by Th22;

theorem :: SEQ_1:50

for seq2, seq, seq1 being Real_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq

proof end;

theorem Th51: :: SEQ_1:51

for seq1, seq2, seq being Real_Sequence st seq1 is being_not_0 holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

proof end;

theorem Th52: :: SEQ_1:52

for r being real number
for seq being Real_Sequence st r <> 0 & seq is being_not_0 holds
r (#) seq is being_not_0

proof end;

theorem :: SEQ_1:53

for seq being Real_Sequence st seq is being_not_0 holds
- seq is being_not_0

proof end;

theorem Th54: :: SEQ_1:54

for r being real number
for seq being Real_Sequence holds (r (#) seq) " = (r " ) (#) (seq " )

proof end;

Lm1: (- 1) " = - 1
;

theorem Th55: :: SEQ_1:55

for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq " )

proof end;

theorem :: SEQ_1:56

for seq1, seq being Real_Sequence holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

proof end;

theorem Th57: :: SEQ_1:57

for seq1, seq, seq1' being Real_Sequence holds
( (seq1 /" seq) + (seq1' /" seq) = (seq1 + seq1') /" seq & (seq1 /" seq) - (seq1' /" seq) = (seq1 - seq1') /" seq ) by Th23, Th28;

theorem :: SEQ_1:58

for seq, seq', seq1, seq1' being Real_Sequence st seq is being_not_0 & seq' is being_not_0 holds
( (seq1 /" seq) + (seq1' /" seq') = ((seq1 (#) seq') + (seq1' (#) seq)) /" (seq (#) seq') & (seq1 /" seq) - (seq1' /" seq') = ((seq1 (#) seq') - (seq1' (#) seq)) /" (seq (#) seq') )

proof end;

theorem :: SEQ_1:59

for seq1', seq, seq', seq1 being Real_Sequence holds (seq1' /" seq) /" (seq' /" seq1) = (seq1' (#) seq1) /" (seq (#) seq')

proof end;

theorem Th60: :: SEQ_1:60

for seq, seq' being Real_Sequence holds abs (seq (#) seq') = (abs seq) (#) (abs seq')

proof end;

theorem :: SEQ_1:61

for seq being Real_Sequence st seq is being_not_0 holds
abs seq is being_not_0

proof end;

theorem Th62: :: SEQ_1:62

for seq being Real_Sequence holds (abs seq) " = abs (seq " )

proof end;

theorem :: SEQ_1:63

for seq', seq being Real_Sequence holds abs (seq' /" seq) = (abs seq') /" (abs seq)

proof end;

theorem :: SEQ_1:64

for r being real number
for seq being Real_Sequence holds abs (r (#) seq) = (abs r) (#) (abs seq)

proof end;