:: COMSEQ_1 semantic presentation

definition

mode Complex_Sequence is Function of NAT , COMPLEX ;

end;

theorem Th1: :: COMSEQ_1:1

for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )

proof end;

theorem Th2: :: COMSEQ_1:2

for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for n being Nat holds f . n is Element of COMPLEX ) ) )

proof end;

definition

let seq be Complex_Sequence;
let n be Nat;
:: original: .
redefine func seq . n -> Element of COMPLEX ;
coherence by Th2;

end;

scheme :: COMSEQ_1:sch 1
ExComplexSeq{ F₁( Nat) -> Element of COMPLEX } :

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

proof end;

definition

let IT be Complex_Sequence;
attr IT is non-zero means :Def1: :: COMSEQ_1:def 1
rng IT c= COMPLEX \ {0c };

end;

:: deftheorem Def1 defines non-zero COMSEQ_1:def 1 :

theorem Th3: :: COMSEQ_1:3

for seq being Complex_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )

proof end;

registration

cluster non-zero Relation of NAT , COMPLEX ;
existence

proof end;

end;

theorem Th4: :: COMSEQ_1:4

for seq being Complex_Sequence holds
( seq is non-zero iff for n being Nat holds seq . n <> 0c )

proof end;

theorem :: COMSEQ_1:5

canceled;

theorem Th6: :: COMSEQ_1:6

for seq, seq1 being Complex_Sequence st ( for n being Nat holds seq . n = seq1 . n ) holds
seq = seq1

proof end;

theorem :: COMSEQ_1:7

for r being Element of COMPLEX ex seq being Complex_Sequence st rng seq = {r}

proof end;

definition

let C be non empty set ;
let f1, f2 be PartFunc of C, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (f1 /. $1) + (f2 /. $1);
defpred S₁[ set ] means $1 in (dom f1) /\ (dom f2);
set X = (dom f1) /\ (dom f2);
func f1 + f2 -> PartFunc of C, COMPLEX means :Def2: :: COMSEQ_1:def 2
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds
it . c = (f1 /. c) + (f2 /. c) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
deffunc H₂( set ) -> Element of COMPLEX = (f1 /. $1) * (f2 /. $1);
func f1 (#) f2 -> PartFunc of C, COMPLEX means :Def3: :: COMSEQ_1:def 3
( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds
it . c = (f1 /. c) * (f2 /. c) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines + COMSEQ_1:def 2 :

:: deftheorem Def3 defines (#) COMSEQ_1:def 3 :

definition

let C be non empty set ;
let f1, f2 be Function of C, COMPLEX ;
redefine func f1 + f2 means :Def4: :: COMSEQ_1:def 4
( dom it = C & ( for c being Element of C holds it . c = (f1 . c) + (f2 . c) ) );
compatibility

proof end;

redefine func f1 (#) f2 means :Def5: :: COMSEQ_1:def 5
( dom it = C & ( for c being Element of C holds it . c = (f1 . c) * (f2 . c) ) );
compatibility

proof end;

end;

:: deftheorem Def4 defines + COMSEQ_1:def 4 :

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

registration

let C be non empty set ;
let seq1, seq2 be Function of C, COMPLEX ;
cluster seq1 + seq2 -> total ;
coherence

proof end;

cluster seq1 (#) seq2 -> total ;
coherence

proof end;

end;

definition

let C be non empty set ;
let f be PartFunc of C, COMPLEX ;
let r be complex number ;
func r (#) f -> PartFunc of C, COMPLEX means :Def6: :: COMSEQ_1:def 6
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = r * (f /. c) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let C be non empty set ;
let f be Function of C, COMPLEX ;
let r be complex number ;
redefine func r (#) f means :Def7: :: COMSEQ_1:def 7
( dom it = C & ( for n being Element of C holds it . n = r * (f . n) ) );
compatibility

proof end;

end;

:: deftheorem Def7 defines (#) COMSEQ_1:def 7 :

registration

let C be non empty set ;
let seq be Function of C, COMPLEX ;
let r be complex number ;
cluster r (#) seq -> total ;
coherence

proof end;

end;

definition

let C be non empty set ;
let f be PartFunc of C, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = - (f /. $1);
func - f -> PartFunc of C, COMPLEX means :Def8: :: COMSEQ_1:def 8
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = - (f /. c) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines - COMSEQ_1:def 8 :

definition

let C be non empty set ;
let f be Function of C, COMPLEX ;
redefine func - f means :Def9: :: COMSEQ_1:def 9
( dom it = C & ( for n being Element of C holds it . n = - (f . n) ) );
compatibility

proof end;

end;

:: deftheorem Def9 defines - COMSEQ_1:def 9 :

registration

let C be non empty set ;
let seq be Function of C, COMPLEX ;
cluster - seq -> total ;
coherence

proof end;

end;

definition

let C be non empty set ;
let f1, f2 be PartFunc of C, COMPLEX ;
func f1 - f2 -> PartFunc of C, COMPLEX equals :: COMSEQ_1:def 10
f1 + (- f2);
correctness ;

end;

:: deftheorem defines - COMSEQ_1:def 10 :

registration

let C be non empty set ;
let f1, f2 be Function of C, COMPLEX ;
cluster f1 - f2 -> total ;
correctness ;

end;

definition

let seq be Complex_Sequence;
func seq " -> Complex_Sequence means :Def11: :: COMSEQ_1:def 11
for n being Nat holds it . n = (seq . n) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines " COMSEQ_1:def 11 :

definition

let seq1, seq be Complex_Sequence;
func seq1 /" seq -> Complex_Sequence equals :: COMSEQ_1:def 12
seq1 (#) (seq " );
correctness ;

end;

:: deftheorem defines /" COMSEQ_1:def 12 :

definition

let C be non empty set ;
let f be PartFunc of C, COMPLEX ;
deffunc H₁( set ) -> Element of REAL = |.(f /. $1).|;
func |.f.| -> PartFunc of C, REAL means :Def13: :: COMSEQ_1:def 13
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = |.(f /. c).| ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines |. COMSEQ_1:def 13 :

definition

let C be non empty set ;
let seq be Function of C, COMPLEX ;
redefine func |.seq.| means :Def14: :: COMSEQ_1:def 14
( dom it = C & ( for n being Element of C holds it . n = |.(seq . n).| ) );
compatibility

proof end;

end;

:: deftheorem Def14 defines |. COMSEQ_1:def 14 :

registration

let C be non empty set ;
let seq be Function of C, COMPLEX ;
cluster |.seq.| -> total ;
coherence

proof end;

end;

theorem :: COMSEQ_1:8

canceled;

theorem Th9: :: COMSEQ_1:9

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

proof end;

theorem :: COMSEQ_1:10

canceled;

theorem Th11: :: COMSEQ_1:11

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

proof end;

theorem Th12: :: COMSEQ_1:12

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

proof end;

theorem :: COMSEQ_1:13

for seq3, seq1, seq2 being Complex_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th12;

theorem Th14: :: COMSEQ_1:14

for seq being Complex_Sequence holds - seq = (- 1r ) (#) seq

proof end;

theorem Th15: :: COMSEQ_1:15

for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2

proof end;

theorem Th16: :: COMSEQ_1:16

for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)

proof end;

theorem Th17: :: COMSEQ_1:17

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

proof end;

theorem :: COMSEQ_1:18

for seq3, seq1, seq2 being Complex_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th17;

theorem Th19: :: COMSEQ_1:19

for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)

proof end;

theorem Th20: :: COMSEQ_1:20

for r, p being Element of COMPLEX
for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)

proof end;

theorem Th21: :: COMSEQ_1:21

for r being Element of COMPLEX
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)

proof end;

theorem Th22: :: COMSEQ_1:22

for r being Element of COMPLEX
for seq1, seq being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq by Th15;

theorem :: COMSEQ_1:23

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

proof end;

theorem Th24: :: COMSEQ_1:24

for seq being Complex_Sequence holds 1r (#) seq = seq

proof end;

theorem Th25: :: COMSEQ_1:25

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

proof end;

theorem Th26: :: COMSEQ_1:26

for seq1, seq2 being Complex_Sequence holds seq1 - (- seq2) = seq1 + seq2 by Th25;

theorem :: COMSEQ_1:27

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

proof end;

theorem :: COMSEQ_1:28

for seq1, seq2, seq3 being Complex_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3 by Th9;

theorem :: COMSEQ_1:29

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

proof end;

theorem Th30: :: COMSEQ_1:30

for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero

proof end;

theorem Th31: :: COMSEQ_1:31

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

proof end;

theorem Th32: :: COMSEQ_1:32

for seq, seq1 being Complex_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )

proof end;

theorem Th33: :: COMSEQ_1:33

for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
(seq " ) (#) (seq1 " ) = (seq (#) seq1) "

proof end;

theorem :: COMSEQ_1:34

for seq, seq1 being Complex_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1

proof end;

theorem :: COMSEQ_1:35

for seq, seq1, seq', seq1' being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
(seq' /" seq) (#) (seq1' /" seq1) = (seq' (#) seq1') /" (seq (#) seq1)

proof end;

theorem :: COMSEQ_1:36

for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero

proof end;

theorem Th37: :: COMSEQ_1:37

for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
(seq /" seq1) " = seq1 /" seq

proof end;

theorem Th38: :: COMSEQ_1:38

for seq2, seq1, seq being Complex_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq by Th11;

theorem :: COMSEQ_1:39

for seq, seq1, seq2 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq

proof end;

theorem Th40: :: COMSEQ_1:40

for seq, seq1, seq2 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)

proof end;

theorem Th41: :: COMSEQ_1:41

for r being Element of COMPLEX
for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero

proof end;

theorem :: COMSEQ_1:42

for seq being Complex_Sequence st seq is non-zero holds
- seq is non-zero

proof end;

theorem Th43: :: COMSEQ_1:43

for r being Element of COMPLEX
for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
(r (#) seq) " = (r " ) (#) (seq " )

proof end;

theorem Th44: :: COMSEQ_1:44

for seq being Complex_Sequence st seq is non-zero holds
(- seq) " = (- 1r ) (#) (seq " )

proof end;

theorem :: COMSEQ_1:45

for seq, seq1 being Complex_Sequence st seq is non-zero holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )

proof end;

theorem Th46: :: COMSEQ_1:46

for seq1, seq, seq1' being Complex_Sequence holds
( (seq1 /" seq) + (seq1' /" seq) = (seq1 + seq1') /" seq & (seq1 /" seq) - (seq1' /" seq) = (seq1 - seq1') /" seq ) by Th12, Th17;

theorem :: COMSEQ_1:47

for seq, seq', seq1, seq1' being Complex_Sequence st seq is non-zero & seq' is non-zero holds
( (seq1 /" seq) + (seq1' /" seq') = ((seq1 (#) seq') + (seq1' (#) seq)) /" (seq (#) seq') & (seq1 /" seq) - (seq1' /" seq') = ((seq1 (#) seq') - (seq1' (#) seq)) /" (seq (#) seq') )

proof end;

theorem :: COMSEQ_1:48

for seq, seq', seq1, seq1' being Complex_Sequence st seq is non-zero & seq' is non-zero & seq1 is non-zero holds
(seq1' /" seq) /" (seq' /" seq1) = (seq1' (#) seq1) /" (seq (#) seq')

proof end;

theorem Th49: :: COMSEQ_1:49

for seq, seq' being Complex_Sequence holds |.(seq (#) seq').| = |.seq.| (#) |.seq'.|

proof end;

theorem :: COMSEQ_1:50

for seq being Complex_Sequence st seq is non-zero holds
|.seq.| is_not_0

proof end;

theorem Th51: :: COMSEQ_1:51

for seq being Complex_Sequence holds |.seq.| " = |.(seq " ).|

proof end;

theorem :: COMSEQ_1:52

for seq', seq being Complex_Sequence holds |.(seq' /" seq).| = |.seq'.| /" |.seq.|

proof end;

theorem :: COMSEQ_1:53

for r being Element of COMPLEX
for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|

proof end;