:: CLVECT_2 semantic presentation

deffunc H₁( ComplexUnitarySpace) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is convergent means :Def1: :: CLVECT_2:def 1
ex b₁ being Point of a₁ st
for b₂ being Real st b₂ > 0 holds
ex b₃ being Nat st
for b₄ being Nat st b₄ >= b₃ holds
dist (a₂ . b₄),b₁ < b₂;

end;

:: deftheorem Def1 defines convergent CLVECT_2:def 1 :

theorem Th1: :: CLVECT_2:1

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is convergent

proof end;

theorem Th2: :: CLVECT_2:2

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
b₃ . b₅ = b₂ . b₅ holds
b₃ is convergent

proof end;

theorem Th3: :: CLVECT_2:3

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ + b₃ is convergent

proof end;

theorem Th4: :: CLVECT_2:4

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ - b₃ is convergent

proof end;

theorem Th5: :: CLVECT_2:5

for b₁ being ComplexUnitarySpace
for b₂ being Complex
for b₃ being sequence of b₁ st b₃ is convergent holds
b₂ * b₃ is convergent

proof end;

theorem Th6: :: CLVECT_2:6

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
- b₂ is convergent

proof end;

theorem Th7: :: CLVECT_2:7

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ + b₂ is convergent

proof end;

theorem Th8: :: CLVECT_2:8

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ - b₂ is convergent

proof end;

theorem Th9: :: CLVECT_2:9

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is convergent iff ex b₃ being Point of b₁ st
for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₂ . b₆) - b₃).|| < b₄ )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
assume E11: c₂ is convergent ;
func lim c₂ -> Point of a₁ means :Def2: :: CLVECT_2:def 2
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
dist (a₂ . b₃),a₃ < b₁;
existence by E11, Def1;
uniqueness

proof end;

end;

:: deftheorem Def2 defines lim CLVECT_2:def 2 :

theorem Th10: :: CLVECT_2:10

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is constant & b₂ in rng b₃ holds
lim b₃ = b₂

proof end;

theorem Th11: :: CLVECT_2:11

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is constant & ex b₄ being Nat st b₃ . b₄ = b₂ holds
lim b₃ = b₂

proof end;

theorem Th12: :: CLVECT_2:12

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₃ . b₅ = b₂ . b₅ holds
lim b₂ = lim b₃

proof end;

theorem Th13: :: CLVECT_2:13

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ + b₃) = (lim b₂) + (lim b₃)

proof end;

theorem Th14: :: CLVECT_2:14

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ - b₃) = (lim b₂) - (lim b₃)

proof end;

theorem Th15: :: CLVECT_2:15

for b₁ being ComplexUnitarySpace
for b₂ being Complex
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₂ * b₃) = b₂ * (lim b₃)

proof end;

theorem Th16: :: CLVECT_2:16

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
lim (- b₂) = - (lim b₂)

proof end;

theorem Th17: :: CLVECT_2:17

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ + b₂) = (lim b₃) + b₂

proof end;

theorem Th18: :: CLVECT_2:18

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ - b₂) = (lim b₃) - b₂

proof end;

theorem Th19: :: CLVECT_2:19

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
( lim b₃ = b₂ iff for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₃ . b₆) - b₂).|| < b₄ )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
func ||.c₂.|| -> Real_Sequence means :Def3: :: CLVECT_2:def 3
for b₁ being Nat holds a₃ . b₁ = ||.(a₂ . b₁).||;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ||. CLVECT_2:def 3 :

theorem Th20: :: CLVECT_2:20

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
||.b₂.|| is convergent

proof end;

theorem Th21: :: CLVECT_2:21

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.b₃.|| is convergent & lim ||.b₃.|| = ||.b₂.|| )

proof end;

theorem Th22: :: CLVECT_2:22

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(b₃ - b₂).|| is convergent & lim ||.(b₃ - b₂).|| = 0 )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Point of c₁;
func dist c₂,c₃ -> Real_Sequence means :Def4: :: CLVECT_2:def 4
for b₁ being Nat holds a₄ . b₁ = dist (a₂ . b₁),a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines dist CLVECT_2:def 4 :

theorem Th23: :: CLVECT_2:23

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
dist b₃,b₂ is convergent

proof end;

theorem Th24: :: CLVECT_2:24

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( dist b₃,b₂ is convergent & lim (dist b₃,b₂) = 0 )

proof end;

theorem Th25: :: CLVECT_2:25

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.(b₄ + b₅).|| is convergent & lim ||.(b₄ + b₅).|| = ||.(b₂ + b₃).|| )

proof end;

theorem Th26: :: CLVECT_2:26

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.((b₄ + b₅) - (b₂ + b₃)).|| is convergent & lim ||.((b₄ + b₅) - (b₂ + b₃)).|| = 0 )

proof end;

theorem Th27: :: CLVECT_2:27

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.(b₄ - b₅).|| is convergent & lim ||.(b₄ - b₅).|| = ||.(b₂ - b₃).|| )

proof end;

theorem Th28: :: CLVECT_2:28

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( ||.((b₄ - b₅) - (b₂ - b₃)).|| is convergent & lim ||.((b₄ - b₅) - (b₂ - b₃)).|| = 0 )

proof end;

theorem Th29: :: CLVECT_2:29

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Complex
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₃ * b₄).|| is convergent & lim ||.(b₃ * b₄).|| = ||.(b₃ * b₂).|| )

proof end;

theorem Th30: :: CLVECT_2:30

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Complex
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₃ * b₄) - (b₃ * b₂)).|| is convergent & lim ||.((b₃ * b₄) - (b₃ * b₂)).|| = 0 )

proof end;

theorem Th31: :: CLVECT_2:31

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(- b₃).|| is convergent & lim ||.(- b₃).|| = ||.(- b₂).|| )

proof end;

theorem Th32: :: CLVECT_2:32

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.((- b₃) - (- b₂)).|| is convergent & lim ||.((- b₃) - (- b₂)).|| = 0 )

proof end;

Lemma26: for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₄ + b₃).|| is convergent & lim ||.(b₄ + b₃).|| = ||.(b₂ + b₃).|| )

proof end;

theorem Th33: :: CLVECT_2:33

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₄ + b₃) - (b₂ + b₃)).|| is convergent & lim ||.((b₄ + b₃) - (b₂ + b₃)).|| = 0 )

proof end;

theorem Th34: :: CLVECT_2:34

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.(b₄ - b₃).|| is convergent & lim ||.(b₄ - b₃).|| = ||.(b₂ - b₃).|| )

proof end;

theorem Th35: :: CLVECT_2:35

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( ||.((b₄ - b₃) - (b₂ - b₃)).|| is convergent & lim ||.((b₄ - b₃) - (b₂ - b₃)).|| = 0 )

proof end;

theorem Th36: :: CLVECT_2:36

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( dist (b₄ + b₅),(b₂ + b₃) is convergent & lim (dist (b₄ + b₅),(b₂ + b₃)) = 0 )

proof end;

theorem Th37: :: CLVECT_2:37

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ & b₅ is convergent & lim b₅ = b₃ holds
( dist (b₄ - b₅),(b₂ - b₃) is convergent & lim (dist (b₄ - b₅),(b₂ - b₃)) = 0 )

proof end;

theorem Th38: :: CLVECT_2:38

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Complex
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( dist (b₃ * b₄),(b₃ * b₂) is convergent & lim (dist (b₃ * b₄),(b₃ * b₂)) = 0 )

proof end;

theorem Th39: :: CLVECT_2:39

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being sequence of b₁ st b₄ is convergent & lim b₄ = b₂ holds
( dist (b₄ + b₃),(b₂ + b₃) is convergent & lim (dist (b₄ + b₃),(b₂ + b₃)) = 0 )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be Point of c₁;
let c₃ be Real;
func Ball c₂,c₃ -> Subset of a₁ equals :: CLVECT_2:def 5
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| < a₃ } ;
coherence

proof end;

func cl_Ball c₂,c₃ -> Subset of a₁ equals :: CLVECT_2:def 6
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| <= a₃ } ;
coherence

proof end;

func Sphere c₂,c₃ -> Subset of a₁ equals :: CLVECT_2:def 7
{ b₁ where B is Point of a₁ : ||.(a₂ - b₁).|| = a₃ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines Ball CLVECT_2:def 5 :

:: deftheorem Def6 defines cl_Ball CLVECT_2:def 6 :

:: deftheorem Def7 defines Sphere CLVECT_2:def 7 :

theorem Th40: :: CLVECT_2:40

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Ball b₃,b₄ iff ||.(b₃ - b₂).|| < b₄ )

proof end;

theorem Th41: :: CLVECT_2:41

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Ball b₃,b₄ iff dist b₃,b₂ < b₄ )

proof end;

theorem Th42: :: CLVECT_2:42

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Real st b₃ > 0 holds
b₂ in Ball b₂,b₃

proof end;

theorem Th43: :: CLVECT_2:43

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₂ in Ball b₃,b₅ & b₄ in Ball b₃,b₅ holds
dist b₂,b₄ < 2 * b₅

proof end;

theorem Th44: :: CLVECT_2:44

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₂ in Ball b₃,b₅ holds
b₂ - b₄ in Ball (b₃ - b₄),b₅

proof end;

theorem Th45: :: CLVECT_2:45

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Ball b₃,b₄ holds
b₂ - b₃ in Ball (0. b₁),b₄

proof end;

theorem Th46: :: CLVECT_2:46

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄, b₅ being Real st b₂ in Ball b₃,b₄ & b₄ <= b₅ holds
b₂ in Ball b₃,b₅

proof end;

theorem Th47: :: CLVECT_2:47

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in cl_Ball b₃,b₄ iff ||.(b₃ - b₂).|| <= b₄ )

proof end;

theorem Th48: :: CLVECT_2:48

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in cl_Ball b₃,b₄ iff dist b₃,b₂ <= b₄ )

proof end;

theorem Th49: :: CLVECT_2:49

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Real st b₃ >= 0 holds
b₂ in cl_Ball b₂,b₃

proof end;

theorem Th50: :: CLVECT_2:50

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Ball b₃,b₄ holds
b₂ in cl_Ball b₃,b₄

proof end;

theorem Th51: :: CLVECT_2:51

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Sphere b₃,b₄ iff ||.(b₃ - b₂).|| = b₄ )

proof end;

theorem Th52: :: CLVECT_2:52

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real holds
( b₂ in Sphere b₃,b₄ iff dist b₃,b₂ = b₄ )

proof end;

theorem Th53: :: CLVECT_2:53

for b₁ being ComplexUnitarySpace
for b₂, b₃ being Point of b₁
for b₄ being Real st b₂ in Sphere b₃,b₄ holds
b₂ in cl_Ball b₃,b₄

proof end;

theorem Th54: :: CLVECT_2:54

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds Ball b₂,b₃ c= cl_Ball b₂,b₃

proof end;

theorem Th55: :: CLVECT_2:55

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds Sphere b₂,b₃ c= cl_Ball b₂,b₃

proof end;

theorem Th56: :: CLVECT_2:56

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being Real holds (Ball b₂,b₃) \/ (Sphere b₂,b₃) = cl_Ball b₂,b₃

proof end;

deffunc H₂( ComplexUnitarySpace) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is Cauchy means :Def8: :: CLVECT_2:def 8
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₃ >= b₂ & b₄ >= b₂ holds
dist (a₂ . b₃),(a₂ . b₄) < b₁;

end;

:: deftheorem Def8 defines Cauchy CLVECT_2:def 8 :

theorem Th57: :: CLVECT_2:57

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is Cauchy

proof end;

theorem Th58: :: CLVECT_2:58

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds
( b₂ is Cauchy iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅, b₆ being Nat st b₅ >= b₄ & b₆ >= b₄ holds
||.((b₂ . b₅) - (b₂ . b₆)).|| < b₃ )

proof end;

theorem Th59: :: CLVECT_2:59

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & b₃ is Cauchy holds
b₂ + b₃ is Cauchy

proof end;

theorem Th60: :: CLVECT_2:60

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & b₃ is Cauchy holds
b₂ - b₃ is Cauchy

proof end;

theorem Th61: :: CLVECT_2:61

for b₁ being ComplexUnitarySpace
for b₂ being Complex
for b₃ being sequence of b₁ st b₃ is Cauchy holds
b₂ * b₃ is Cauchy

proof end;

theorem Th62: :: CLVECT_2:62

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is Cauchy holds
- b₂ is Cauchy

proof end;

theorem Th63: :: CLVECT_2:63

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is Cauchy holds
b₃ + b₂ is Cauchy

proof end;

theorem Th64: :: CLVECT_2:64

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is Cauchy holds
b₃ - b₂ is Cauchy

proof end;

theorem Th65: :: CLVECT_2:65

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
b₂ is Cauchy

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂, c₃ be sequence of c₁;
pred c₂ is_compared_to c₃ means :Def9: :: CLVECT_2:def 9
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
dist (a₂ . b₃),(a₃ . b₃) < b₁;

end;

:: deftheorem Def9 defines is_compared_to CLVECT_2:def 9 :

theorem Th66: :: CLVECT_2:66

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ is_compared_to b₂

proof end;

theorem Th67: :: CLVECT_2:67

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is_compared_to b₃ holds
b₃ is_compared_to b₂

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂, c₃ be sequence of c₁;
redefine pred is_compared_to as c₂ is_compared_to c₃;
reflexivity by Th66;
symmetry by Th67;

end;

theorem Th68: :: CLVECT_2:68

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is_compared_to b₃ & b₃ is_compared_to b₄ holds
b₂ is_compared_to b₄

proof end;

theorem Th69: :: CLVECT_2:69

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ holds
( b₂ is_compared_to b₃ iff for b₄ being Real st b₄ > 0 holds
ex b₅ being Nat st
for b₆ being Nat st b₆ >= b₅ holds
||.((b₂ . b₆) - (b₃ . b₆)).|| < b₄ )

proof end;

theorem Th70: :: CLVECT_2:70

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st ex b₄ being Nat st
for b₅ being Nat st b₅ >= b₄ holds
b₂ . b₅ = b₃ . b₅ holds
b₂ is_compared_to b₃

proof end;

theorem Th71: :: CLVECT_2:71

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & b₂ is_compared_to b₃ holds
b₃ is Cauchy

proof end;

theorem Th72: :: CLVECT_2:72

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₂ is_compared_to b₃ holds
b₃ is convergent

proof end;

theorem Th73: :: CLVECT_2:73

for b₁ being ComplexUnitarySpace
for b₂ being Point of b₁
for b₃, b₄ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ & b₃ is_compared_to b₄ holds
( b₄ is convergent & lim b₄ = b₂ )

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
attr a₂ is bounded means :Def10: :: CLVECT_2:def 10
ex b₁ being Real st
( b₁ > 0 & ( for b₂ being Nat holds ||.(a₂ . b₂).|| <= b₁ ) );

end;

:: deftheorem Def10 defines bounded CLVECT_2:def 10 :

theorem Th74: :: CLVECT_2:74

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is bounded holds
b₂ + b₃ is bounded

proof end;

theorem Th75: :: CLVECT_2:75

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is bounded holds
- b₂ is bounded

proof end;

theorem Th76: :: CLVECT_2:76

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is bounded holds
b₂ - b₃ is bounded

proof end;

theorem Th77: :: CLVECT_2:77

for b₁ being ComplexUnitarySpace
for b₂ being Complex
for b₃ being sequence of b₁ st b₃ is bounded holds
b₂ * b₃ is bounded

proof end;

theorem Th78: :: CLVECT_2:78

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is bounded

proof end;

theorem Th79: :: CLVECT_2:79

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Nat st b₅ <= b₃ holds
||.(b₂ . b₅).|| < b₄ ) )

proof end;

theorem Th80: :: CLVECT_2:80

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₂ is convergent holds
b₂ is bounded

proof end;

theorem Th81: :: CLVECT_2:81

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₂ is_compared_to b₃ holds
b₃ is bounded

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be increasing Seq_of_Nat;
let c₃ be sequence of c₁;
redefine func * as c₃ * c₂ -> sequence of a₁;
coherence

proof end;

end;

theorem Th82: :: CLVECT_2:82

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being increasing Seq_of_Nat
for b₄ being Nat holds (b₂ * b₃) . b₄ = b₂ . (b₃ . b₄)

proof end;

theorem Th83: :: CLVECT_2:83

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ is subsequence of b₂

proof end;

theorem Th84: :: CLVECT_2:84

for b₁ being ComplexUnitarySpace
for b₂, b₃, b₄ being sequence of b₁ st b₂ is subsequence of b₃ & b₃ is subsequence of b₄ holds
b₂ is subsequence of b₄

proof end;

theorem Th85: :: CLVECT_2:85

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is constant & b₃ is subsequence of b₂ holds
b₃ is constant

proof end;

theorem Th86: :: CLVECT_2:86

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is constant & b₃ is subsequence of b₂ holds
b₂ = b₃

proof end;

theorem Th87: :: CLVECT_2:87

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is bounded & b₃ is subsequence of b₂ holds
b₃ is bounded

proof end;

theorem Th88: :: CLVECT_2:88

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is subsequence of b₂ holds
b₃ is convergent

proof end;

theorem Th89: :: CLVECT_2:89

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is subsequence of b₃ & b₃ is convergent holds
lim b₂ = lim b₃

proof end;

theorem Th90: :: CLVECT_2:90

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & b₃ is subsequence of b₂ holds
b₃ is Cauchy

proof end;

definition

let c₁ be ComplexUnitarySpace;
let c₂ be sequence of c₁;
let c₃ be Nat;
func c₂ ^\ c₃ -> sequence of a₁ means :Def11: :: CLVECT_2:def 11
for b₁ being Nat holds a₄ . b₁ = a₂ . (b₁ + a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines ^\ CLVECT_2:def 11 :

theorem Th91: :: CLVECT_2:91

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ holds b₂ ^\ 0 = b₂

proof end;

theorem Th92: :: CLVECT_2:92

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = (b₂ ^\ b₄) ^\ b₃

proof end;

theorem Th93: :: CLVECT_2:93

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃, b₄ being Nat holds (b₂ ^\ b₃) ^\ b₄ = b₂ ^\ (b₃ + b₄)

proof end;

theorem Th94: :: CLVECT_2:94

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat holds (b₂ + b₃) ^\ b₄ = (b₂ ^\ b₄) + (b₃ ^\ b₄)

proof end;

theorem Th95: :: CLVECT_2:95

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds (- b₂) ^\ b₃ = - (b₂ ^\ b₃)

proof end;

theorem Th96: :: CLVECT_2:96

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat holds (b₂ - b₃) ^\ b₄ = (b₂ ^\ b₄) - (b₃ ^\ b₄)

proof end;

theorem Th97: :: CLVECT_2:97

for b₁ being ComplexUnitarySpace
for b₂ being Complex
for b₃ being sequence of b₁
for b₄ being Nat holds (b₂ * b₃) ^\ b₄ = b₂ * (b₃ ^\ b₄)

proof end;

theorem Th98: :: CLVECT_2:98

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat
for b₄ being increasing Seq_of_Nat holds (b₂ * b₄) ^\ b₃ = b₂ * (b₄ ^\ b₃)

proof end;

theorem Th99: :: CLVECT_2:99

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat holds b₂ ^\ b₃ is subsequence of b₂

proof end;

theorem Th100: :: CLVECT_2:100

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is convergent holds
( b₂ ^\ b₃ is convergent & lim (b₂ ^\ b₃) = lim b₂ )

proof end;

theorem Th101: :: CLVECT_2:101

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
b₃ is convergent

proof end;

theorem Th102: :: CLVECT_2:102

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & ex b₄ being Nat st b₂ = b₃ ^\ b₄ holds
b₃ is Cauchy

proof end;

theorem Th103: :: CLVECT_2:103

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is Cauchy holds
b₂ ^\ b₃ is Cauchy

proof end;

theorem Th104: :: CLVECT_2:104

for b₁ being ComplexUnitarySpace
for b₂, b₃ being sequence of b₁
for b₄ being Nat st b₂ is_compared_to b₃ holds
b₂ ^\ b₄ is_compared_to b₃ ^\ b₄

proof end;

theorem Th105: :: CLVECT_2:105

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is bounded holds
b₂ ^\ b₃ is bounded

proof end;

theorem Th106: :: CLVECT_2:106

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁
for b₃ being Nat st b₂ is constant holds
b₂ ^\ b₃ is constant

proof end;

definition

let c₁ be ComplexUnitarySpace;
attr a₁ is complete means :Def12: :: CLVECT_2:def 12
for b₁ being sequence of a₁ st b₁ is Cauchy holds
b₁ is convergent;

end;

:: deftheorem Def12 defines complete CLVECT_2:def 12 :

theorem Th107: :: CLVECT_2:107

for b₁ being ComplexUnitarySpace
for b₂ being sequence of b₁ st b₁ is complete & b₂ is Cauchy holds
b₂ is bounded

proof end;

definition

let c₁ be ComplexUnitarySpace;
attr a₁ is Hilbert means :: CLVECT_2:def 13
( a₁ is ComplexUnitarySpace & a₁ is complete );

end;

:: deftheorem Def13 defines Hilbert CLVECT_2:def 13 :