:: COMSEQ_1 semantic presentation

definition

mode Complex_Sequence is Function of NAT , COMPLEX ;

end;

theorem Th1: :: COMSEQ_1:1

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

proof end;

theorem Th2: :: COMSEQ_1:2

for b₁ being Function holds
( b₁ is Complex_Sequence iff ( dom b₁ = NAT & ( for b₂ being Nat holds b₁ . b₂ is Element of COMPLEX ) ) )

proof end;

definition

let c₁ be Complex_Sequence;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> Element of COMPLEX ;
coherence by Th2;

end;

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

ex b₁ being Complex_Sequence st
for b₂ being Nat holds b₁ . b₂ = F₁(b₂)

proof end;

definition

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

end;

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

theorem Th3: :: COMSEQ_1:3

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

proof end;

registration

cluster non-zero Relation of NAT , COMPLEX ;
existence

proof end;

end;

theorem Th4: :: COMSEQ_1:4

for b₁ being Complex_Sequence holds
( b₁ is non-zero iff for b₂ being Nat holds b₁ . b₂ <> 0c )

proof end;

theorem Th5: :: COMSEQ_1:5

canceled;

theorem Th6: :: COMSEQ_1:6

for b₁, b₂ being Complex_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th7: :: COMSEQ_1:7

for b₁ being Element of COMPLEX ex b₂ being Complex_Sequence st rng b₂ = {b₁}

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be PartFunc of c₁, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (c₂ /. a₁) + (c₃ /. a₁);
defpred S₁[ set ] means a₁ in (dom c₂) /\ (dom c₃);
set c₄ = (dom c₂) /\ (dom c₃);
func c₂ + c₃ -> PartFunc of a₁, COMPLEX means :Def2: :: COMSEQ_1:def 2
( dom a₄ = (dom a₂) /\ (dom a₃) & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = (a₂ /. b₁) + (a₃ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
deffunc H₂( set ) -> Element of COMPLEX = (c₂ /. a₁) * (c₃ /. a₁);
func c₂ (#) c₃ -> PartFunc of a₁, COMPLEX means :Def3: :: COMSEQ_1:def 3
( dom a₄ = (dom a₂) /\ (dom a₃) & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = (a₂ /. b₁) * (a₃ /. b₁) ) );
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 c₂, c₃ be Function of c₁, COMPLEX ;
redefine func c₂ + c₃ -> PartFunc of a₁, COMPLEX means :Def4: :: COMSEQ_1:def 4
( dom a₄ = a₁ & ( for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁) ) );
compatibility

proof end;

redefine func c₂ (#) c₃ -> PartFunc of a₁, COMPLEX means :Def5: :: COMSEQ_1:def 5
( dom a₄ = a₁ & ( for b₁ being Element of a₁ holds a₄ . b₁ = (a₂ . b₁) * (a₃ . b₁) ) );
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 c₂, c₃ be Function of c₁, COMPLEX ;
cluster a₂ + a₃ -> total ;
coherence

proof end;

cluster a₂ (#) a₃ -> total ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, COMPLEX ;
let c₃ be complex number ;
func c₃ (#) c₂ -> PartFunc of a₁, COMPLEX means :Def6: :: COMSEQ_1:def 6
( dom a₄ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₄ holds
a₄ . b₁ = a₃ * (a₂ /. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
let c₃ be complex number ;
redefine func c₃ (#) c₂ -> PartFunc of a₁, COMPLEX means :Def7: :: COMSEQ_1:def 7
( dom a₄ = a₁ & ( for b₁ being Element of a₁ holds a₄ . b₁ = a₃ * (a₂ . b₁) ) );
compatibility

proof end;

end;

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

registration

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
let c₃ be complex number ;
cluster a₃ (#) a₂ -> total ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines - COMSEQ_1:def 8 :

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
redefine func - c₂ -> PartFunc of a₁, COMPLEX means :Def9: :: COMSEQ_1:def 9
( dom a₃ = a₁ & ( for b₁ being Element of a₁ holds a₃ . b₁ = - (a₂ . b₁) ) );
compatibility

proof end;

end;

:: deftheorem Def9 defines - COMSEQ_1:def 9 :

registration

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
cluster - a₂ -> total ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be PartFunc of c₁, COMPLEX ;
func c₂ - c₃ -> PartFunc of a₁, COMPLEX equals :: COMSEQ_1:def 10
a₂ + (- a₃);
correctness ;

end;

:: deftheorem Def10 defines - COMSEQ_1:def 10 :

registration

let c₁ be non empty set ;
let c₂, c₃ be Function of c₁, COMPLEX ;
cluster a₂ - a₃ -> total ;
correctness ;

end;

definition

let c₁ be Complex_Sequence;
func c₁ " -> Complex_Sequence means :Def11: :: COMSEQ_1:def 11
for b₁ being Nat holds a₂ . b₁ = (a₁ . b₁) " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines " COMSEQ_1:def 11 :

definition

let c₁, c₂ be Complex_Sequence;
func c₁ /" c₂ -> Complex_Sequence equals :: COMSEQ_1:def 12
a₁ (#) (a₂ " );
correctness ;

end;

:: deftheorem Def12 defines /" COMSEQ_1:def 12 :

definition

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

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
redefine func |.c₂.| -> PartFunc of a₁, REAL means :Def14: :: COMSEQ_1:def 14
( dom a₃ = a₁ & ( for b₁ being Element of a₁ holds a₃ . b₁ = |.(a₂ . b₁).| ) );
compatibility

proof end;

end;

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

registration

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
cluster |.a₂.| -> total ;
coherence

proof end;

end;

theorem Th8: :: COMSEQ_1:8

canceled;

theorem Th9: :: COMSEQ_1:9

for b₁, b₂, b₃ being Complex_Sequence holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th10: :: COMSEQ_1:10

canceled;

theorem Th11: :: COMSEQ_1:11

for b₁, b₂, b₃ being Complex_Sequence holds (b₁ (#) b₂) (#) b₃ = b₁ (#) (b₂ (#) b₃)

proof end;

theorem Th12: :: COMSEQ_1:12

for b₁, b₂, b₃ being Complex_Sequence holds (b₁ + b₂) (#) b₃ = (b₁ (#) b₃) + (b₂ (#) b₃)

proof end;

theorem Th13: :: COMSEQ_1:13

for b₁, b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ + b₃) = (b₁ (#) b₂) + (b₁ (#) b₃) by Th12;

theorem Th14: :: COMSEQ_1:14

for b₁ being Complex_Sequence holds - b₁ = (- 1r ) (#) b₁

proof end;

theorem Th15: :: COMSEQ_1:15

for b₁ being Element of COMPLEX
for b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ (#) b₃) = (b₁ (#) b₂) (#) b₃

proof end;

theorem Th16: :: COMSEQ_1:16

for b₁ being Element of COMPLEX
for b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ (#) b₃) = b₂ (#) (b₁ (#) b₃)

proof end;

theorem Th17: :: COMSEQ_1:17

for b₁, b₂, b₃ being Complex_Sequence holds (b₁ - b₂) (#) b₃ = (b₁ (#) b₃) - (b₂ (#) b₃)

proof end;

theorem Th18: :: COMSEQ_1:18

for b₁, b₂, b₃ being Complex_Sequence holds (b₁ (#) b₂) - (b₁ (#) b₃) = b₁ (#) (b₂ - b₃) by Th17;

theorem Th19: :: COMSEQ_1:19

for b₁ being Element of COMPLEX
for b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ + b₃) = (b₁ (#) b₂) + (b₁ (#) b₃)

proof end;

theorem Th20: :: COMSEQ_1:20

for b₁, b₂ being Element of COMPLEX
for b₃ being Complex_Sequence holds (b₁ * b₂) (#) b₃ = b₁ (#) (b₂ (#) b₃)

proof end;

theorem Th21: :: COMSEQ_1:21

for b₁ being Element of COMPLEX
for b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ - b₃) = (b₁ (#) b₂) - (b₁ (#) b₃)

proof end;

theorem Th22: :: COMSEQ_1:22

for b₁ being Element of COMPLEX
for b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ /" b₃) = (b₁ (#) b₂) /" b₃ by Th15;

theorem Th23: :: COMSEQ_1:23

for b₁, b₂, b₃ being Complex_Sequence holds b₁ - (b₂ + b₃) = (b₁ - b₂) - b₃

proof end;

theorem Th24: :: COMSEQ_1:24

for b₁ being Complex_Sequence holds 1r (#) b₁ = b₁

proof end;

theorem Th25: :: COMSEQ_1:25

for b₁ being Complex_Sequence holds - (- b₁) = b₁

proof end;

theorem Th26: :: COMSEQ_1:26

for b₁, b₂ being Complex_Sequence holds b₁ - (- b₂) = b₁ + b₂ by Th25;

theorem Th27: :: COMSEQ_1:27

for b₁, b₂, b₃ being Complex_Sequence holds b₁ - (b₂ - b₃) = (b₁ - b₂) + b₃

proof end;

theorem Th28: :: COMSEQ_1:28

for b₁, b₂, b₃ being Complex_Sequence holds b₁ + (b₂ - b₃) = (b₁ + b₂) - b₃ by Th9;

theorem Th29: :: COMSEQ_1:29

for b₁, b₂ being Complex_Sequence holds
( (- b₁) (#) b₂ = - (b₁ (#) b₂) & b₁ (#) (- b₂) = - (b₁ (#) b₂) )

proof end;

theorem Th30: :: COMSEQ_1:30

for b₁ being Complex_Sequence st b₁ is non-zero holds
b₁ " is non-zero

proof end;

theorem Th31: :: COMSEQ_1:31

for b₁ being Complex_Sequence holds (b₁ " ) " = b₁

proof end;

theorem Th32: :: COMSEQ_1:32

for b₁, b₂ being Complex_Sequence holds
( ( b₁ is non-zero & b₂ is non-zero ) iff b₁ (#) b₂ is non-zero )

proof end;

theorem Th33: :: COMSEQ_1:33

for b₁, b₂ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
(b₁ " ) (#) (b₂ " ) = (b₁ (#) b₂) "

proof end;

theorem Th34: :: COMSEQ_1:34

for b₁, b₂ being Complex_Sequence st b₁ is non-zero holds
(b₂ /" b₁) (#) b₁ = b₂

proof end;

theorem Th35: :: COMSEQ_1:35

for b₁, b₂, b₃, b₄ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
(b₃ /" b₁) (#) (b₄ /" b₂) = (b₃ (#) b₄) /" (b₁ (#) b₂)

proof end;

theorem Th36: :: COMSEQ_1:36

for b₁, b₂ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
b₁ /" b₂ is non-zero

proof end;

theorem Th37: :: COMSEQ_1:37

for b₁, b₂ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
(b₁ /" b₂) " = b₂ /" b₁

proof end;

theorem Th38: :: COMSEQ_1:38

for b₁, b₂, b₃ being Complex_Sequence holds b₁ (#) (b₂ /" b₃) = (b₁ (#) b₂) /" b₃ by Th11;

theorem Th39: :: COMSEQ_1:39

for b₁, b₂, b₃ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
b₃ /" (b₁ /" b₂) = (b₃ (#) b₂) /" b₁

proof end;

theorem Th40: :: COMSEQ_1:40

for b₁, b₂, b₃ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
b₃ /" b₁ = (b₃ (#) b₂) /" (b₁ (#) b₂)

proof end;

theorem Th41: :: COMSEQ_1:41

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

proof end;

theorem Th42: :: COMSEQ_1:42

for b₁ being Complex_Sequence st b₁ is non-zero holds
- b₁ is non-zero

proof end;

theorem Th43: :: COMSEQ_1:43

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

proof end;

theorem Th44: :: COMSEQ_1:44

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

proof end;

theorem Th45: :: COMSEQ_1:45

for b₁, b₂ being Complex_Sequence st b₁ is non-zero holds
( - (b₂ /" b₁) = (- b₂) /" b₁ & b₂ /" (- b₁) = - (b₂ /" b₁) )

proof end;

theorem Th46: :: COMSEQ_1:46

for b₁, b₂, b₃ being Complex_Sequence holds
( (b₁ /" b₂) + (b₃ /" b₂) = (b₁ + b₃) /" b₂ & (b₁ /" b₂) - (b₃ /" b₂) = (b₁ - b₃) /" b₂ ) by Th12, Th17;

theorem Th47: :: COMSEQ_1:47

for b₁, b₂, b₃, b₄ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero holds
( (b₃ /" b₁) + (b₄ /" b₂) = ((b₃ (#) b₂) + (b₄ (#) b₁)) /" (b₁ (#) b₂) & (b₃ /" b₁) - (b₄ /" b₂) = ((b₃ (#) b₂) - (b₄ (#) b₁)) /" (b₁ (#) b₂) )

proof end;

theorem Th48: :: COMSEQ_1:48

for b₁, b₂, b₃, b₄ being Complex_Sequence st b₁ is non-zero & b₂ is non-zero & b₃ is non-zero holds
(b₄ /" b₁) /" (b₂ /" b₃) = (b₄ (#) b₃) /" (b₁ (#) b₂)

proof end;

theorem Th49: :: COMSEQ_1:49

for b₁, b₂ being Complex_Sequence holds |.(b₁ (#) b₂).| = |.b₁.| (#) |.b₂.|

proof end;

theorem Th50: :: COMSEQ_1:50

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

proof end;

theorem Th51: :: COMSEQ_1:51

for b₁ being Complex_Sequence holds |.b₁.| " = |.(b₁ " ).|

proof end;

theorem Th52: :: COMSEQ_1:52

for b₁, b₂ being Complex_Sequence holds |.(b₁ /" b₂).| = |.b₁.| /" |.b₂.|

proof end;

theorem Th53: :: COMSEQ_1:53

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence holds |.(b₁ (#) b₂).| = |.b₁.| (#) |.b₂.|

proof end;