:: Cauchy Sequence of Complex Unitary Space
:: by Yasumasa Suzuki and Noboru Endou
::
:: Received March 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users
begin
deffunc
H
1
(
ComplexUnitarySpace
)
->
Element
of the
U1
of $1 =
0.
$1;
theorem
Th1
:
:: CLVECT_3:1
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
holds
(
Partial_Sums
seq1
)
+
(
Partial_Sums
seq2
)
=
Partial_Sums
(
seq1
+
seq2
)
proof
end;
theorem
Th2
:
:: CLVECT_3:2
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
holds
(
Partial_Sums
seq1
)
-
(
Partial_Sums
seq2
)
=
Partial_Sums
(
seq1
-
seq2
)
proof
end;
theorem
Th3
:
:: CLVECT_3:3
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
z
being
Complex
holds
Partial_Sums
(
z
*
seq
)
=
z
*
(
Partial_Sums
seq
)
proof
end;
theorem
:: CLVECT_3:4
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Partial_Sums
(
-
seq
)
=
-
(
Partial_Sums
seq
)
proof
end;
theorem
:: CLVECT_3:5
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
for
z1
,
z2
being
Complex
holds
(
z1
*
(
Partial_Sums
seq1
)
)
+
(
z2
*
(
Partial_Sums
seq2
)
)
=
Partial_Sums
(
(
z1
*
seq1
)
+
(
z2
*
seq2
)
)
proof
end;
definition
let
X
be
ComplexUnitarySpace
;
let
seq
be
sequence
of
X
;
attr
seq
is
summable
means
:
Def1
:
:: CLVECT_3:def 1
Partial_Sums
seq
is
convergent
;
func
Sum
seq
->
Point
of
X
equals
:: CLVECT_3:def 2
lim
(
Partial_Sums
seq
)
;
correctness
coherence
lim
(
Partial_Sums
seq
)
is
Point
of
X
;
;
end;
::
deftheorem
Def1
defines
summable
CLVECT_3:def 1 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
(
seq
is
summable
iff
Partial_Sums
seq
is
convergent
);
::
deftheorem
defines
Sum
CLVECT_3:def 2 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Sum
seq
=
lim
(
Partial_Sums
seq
)
;
theorem
:: CLVECT_3:6
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
st
seq1
is
summable
&
seq2
is
summable
holds
(
seq1
+
seq2
is
summable
&
Sum
(
seq1
+
seq2
)
=
(
Sum
seq1
)
+
(
Sum
seq2
)
)
proof
end;
theorem
:: CLVECT_3:7
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
st
seq1
is
summable
&
seq2
is
summable
holds
(
seq1
-
seq2
is
summable
&
Sum
(
seq1
-
seq2
)
=
(
Sum
seq1
)
-
(
Sum
seq2
)
)
proof
end;
theorem
:: CLVECT_3:8
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
z
being
Complex
st
seq
is
summable
holds
(
z
*
seq
is
summable
&
Sum
(
z
*
seq
)
=
z
*
(
Sum
seq
)
)
proof
end;
theorem
Th9
:
:: CLVECT_3:9
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
st
seq
is
summable
holds
(
seq
is
convergent
&
lim
seq
=
0.
X
)
proof
end;
theorem
Th10
:
:: CLVECT_3:10
for
X
being
ComplexHilbertSpace
for
seq
being
sequence
of
X
holds
(
seq
is
summable
iff for
r
being
Real
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
n
,
m
being
Element
of
NAT
st
n
>=
k
&
m
>=
k
holds
||.
(
(
(
Partial_Sums
seq
)
.
n
)
-
(
(
Partial_Sums
seq
)
.
m
)
)
.||
<
r
)
proof
end;
theorem
:: CLVECT_3:11
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
st
seq
is
summable
holds
Partial_Sums
seq
is
bounded
proof
end;
theorem
Th12
:
:: CLVECT_3:12
for
X
being
ComplexUnitarySpace
for
seq1
,
seq
being
sequence
of
X
st ( for
n
being
Element
of
NAT
holds
seq1
.
n
=
seq
.
0
) holds
Partial_Sums
(
seq
^\
1
)
=
(
(
Partial_Sums
seq
)
^\
1
)
-
seq1
proof
end;
theorem
Th13
:
:: CLVECT_3:13
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
st
seq
is
summable
holds
for
k
being
Element
of
NAT
holds
seq
^\
k
is
summable
proof
end;
theorem
:: CLVECT_3:14
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
st ex
k
being
Element
of
NAT
st
seq
^\
k
is
summable
holds
seq
is
summable
proof
end;
definition
let
X
be
ComplexUnitarySpace
;
let
seq
be
sequence
of
X
;
let
n
be
Element
of
NAT
;
func
Sum
(
seq
,
n
)
->
Point
of
X
equals
:: CLVECT_3:def 3
(
Partial_Sums
seq
)
.
n
;
correctness
coherence
(
Partial_Sums
seq
)
.
n
is
Point
of
X
;
;
end;
::
deftheorem
defines
Sum
CLVECT_3:def 3 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
Sum
(
seq
,
n
)
=
(
Partial_Sums
seq
)
.
n
;
theorem
:: CLVECT_3:15
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Sum
(
seq
,
0
)
=
seq
.
0
by
BHSP_4:def 1
;
theorem
Th16
:
:: CLVECT_3:16
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Sum
(
seq
,1)
=
(
Sum
(
seq
,
0
)
)
+
(
seq
.
1
)
proof
end;
theorem
Th17
:
:: CLVECT_3:17
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Sum
(
seq
,1)
=
(
seq
.
0
)
+
(
seq
.
1
)
proof
end;
theorem
:: CLVECT_3:18
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
Sum
(
seq
,
(
n
+
1
)
)
=
(
Sum
(
seq
,
n
)
)
+
(
seq
.
(
n
+
1
)
)
by
BHSP_4:def 1
;
theorem
Th19
:
:: CLVECT_3:19
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
seq
.
(
n
+
1
)
=
(
Sum
(
seq
,
(
n
+
1
)
)
)
-
(
Sum
(
seq
,
n
)
)
proof
end;
theorem
:: CLVECT_3:20
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
seq
.
1
=
(
Sum
(
seq
,1)
)
-
(
Sum
(
seq
,
0
)
)
proof
end;
definition
let
X
be
ComplexUnitarySpace
;
let
seq
be
sequence
of
X
;
let
n
,
m
be
Element
of
NAT
;
func
Sum
(
seq
,
n
,
m
)
->
Point
of
X
equals
:: CLVECT_3:def 4
(
Sum
(
seq
,
n
)
)
-
(
Sum
(
seq
,
m
)
)
;
correctness
coherence
(
Sum
(
seq
,
n
)
)
-
(
Sum
(
seq
,
m
)
)
is
Point
of
X
;
;
end;
::
deftheorem
defines
Sum
CLVECT_3:def 4 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
,
m
being
Element
of
NAT
holds
Sum
(
seq
,
n
,
m
)
=
(
Sum
(
seq
,
n
)
)
-
(
Sum
(
seq
,
m
)
)
;
theorem
:: CLVECT_3:21
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Sum
(
seq
,1,
0
)
=
seq
.
1
proof
end;
theorem
:: CLVECT_3:22
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
Sum
(
seq
,
(
n
+
1
)
,
n
)
=
seq
.
(
n
+
1
)
by
Th19
;
theorem
Th23
:
:: CLVECT_3:23
for
X
being
ComplexHilbertSpace
for
seq
being
sequence
of
X
holds
(
seq
is
summable
iff for
r
being
Real
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
n
,
m
being
Element
of
NAT
st
n
>=
k
&
m
>=
k
holds
||.
(
(
Sum
(
seq
,
n
)
)
-
(
Sum
(
seq
,
m
)
)
)
.||
<
r
)
proof
end;
theorem
:: CLVECT_3:24
for
X
being
ComplexHilbertSpace
for
seq
being
sequence
of
X
holds
(
seq
is
summable
iff for
r
being
Real
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
n
,
m
being
Element
of
NAT
st
n
>=
k
&
m
>=
k
holds
||.
(
Sum
(
seq
,
n
,
m
)
)
.||
<
r
)
proof
end;
definition
let
Cseq
be
Complex_Sequence
;
let
n
be
Element
of
NAT
;
func
Sum
(
Cseq
,
n
)
->
Complex
equals
:: CLVECT_3:def 5
(
Partial_Sums
Cseq
)
.
n
;
correctness
coherence
(
Partial_Sums
Cseq
)
.
n
is
Complex
;
;
end;
::
deftheorem
defines
Sum
CLVECT_3:def 5 :
for
Cseq
being
Complex_Sequence
for
n
being
Element
of
NAT
holds
Sum
(
Cseq
,
n
)
=
(
Partial_Sums
Cseq
)
.
n
;
definition
let
Cseq
be
Complex_Sequence
;
let
n
,
m
be
Element
of
NAT
;
func
Sum
(
Cseq
,
n
,
m
)
->
Complex
equals
:: CLVECT_3:def 6
(
Sum
(
Cseq
,
n
)
)
-
(
Sum
(
Cseq
,
m
)
)
;
correctness
coherence
(
Sum
(
Cseq
,
n
)
)
-
(
Sum
(
Cseq
,
m
)
)
is
Complex
;
;
end;
::
deftheorem
defines
Sum
CLVECT_3:def 6 :
for
Cseq
being
Complex_Sequence
for
n
,
m
being
Element
of
NAT
holds
Sum
(
Cseq
,
n
,
m
)
=
(
Sum
(
Cseq
,
n
)
)
-
(
Sum
(
Cseq
,
m
)
)
;
definition
let
X
be
ComplexUnitarySpace
;
let
seq
be
sequence
of
X
;
attr
seq
is
absolutely_summable
means
:
Def7
:
:: CLVECT_3:def 7
||.
seq
.||
is
summable
;
end;
::
deftheorem
Def7
defines
absolutely_summable
CLVECT_3:def 7 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
(
seq
is
absolutely_summable
iff
||.
seq
.||
is
summable
);
theorem
:: CLVECT_3:25
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
st
seq1
is
absolutely_summable
&
seq2
is
absolutely_summable
holds
seq1
+
seq2
is
absolutely_summable
proof
end;
theorem
:: CLVECT_3:26
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
z
being
Complex
st
seq
is
absolutely_summable
holds
z
*
seq
is
absolutely_summable
proof
end;
theorem
:: CLVECT_3:27
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
||.
seq
.||
.
n
<=
Rseq
.
n
) &
Rseq
is
summable
holds
seq
is
absolutely_summable
proof
end;
theorem
:: CLVECT_3:28
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
(
seq
.
n
<>
0.
X
&
Rseq
.
n
=
||.
(
seq
.
(
n
+
1
)
)
.||
/
||.
(
seq
.
n
)
.||
) ) &
Rseq
is
convergent
&
lim
Rseq
<
1 holds
seq
is
absolutely_summable
proof
end;
theorem
Th29
:
:: CLVECT_3:29
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
r
being
Real
st
r
>
0
& ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
n
>=
m
holds
||.
(
seq
.
n
)
.||
>=
r
&
seq
is
convergent
holds
lim
seq
<>
0.
X
proof
end;
theorem
Th30
:
:: CLVECT_3:30
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
st ( for
n
being
Element
of
NAT
holds
seq
.
n
<>
0.
X
) & ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
n
>=
m
holds
||.
(
seq
.
(
n
+
1
)
)
.||
/
||.
(
seq
.
n
)
.||
>=
1 holds
not
seq
is
summable
proof
end;
theorem
:: CLVECT_3:31
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
seq
.
n
<>
0.
X
) & ( for
n
being
Element
of
NAT
holds
Rseq
.
n
=
||.
(
seq
.
(
n
+
1
)
)
.||
/
||.
(
seq
.
n
)
.||
) &
Rseq
is
convergent
&
lim
Rseq
>
1 holds
not
seq
is
summable
proof
end;
theorem
:: CLVECT_3:32
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
Rseq
.
n
=
n
-root
||.
(
seq
.
n
)
.||
) &
Rseq
is
convergent
&
lim
Rseq
<
1 holds
seq
is
absolutely_summable
proof
end;
theorem
:: CLVECT_3:33
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
Rseq
.
n
=
n
-root
(
||.
seq
.||
.
n
)
) & ex
m
being
Element
of
NAT
st
for
n
being
Element
of
NAT
st
n
>=
m
holds
Rseq
.
n
>=
1 holds
not
seq
is
summable
proof
end;
theorem
:: CLVECT_3:34
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Rseq
being
Real_Sequence
st ( for
n
being
Element
of
NAT
holds
Rseq
.
n
=
n
-root
(
||.
seq
.||
.
n
)
) &
Rseq
is
convergent
&
lim
Rseq
>
1 holds
not
seq
is
summable
proof
end;
theorem
Th35
:
:: CLVECT_3:35
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
holds
Partial_Sums
||.
seq
.||
is
non-decreasing
proof
end;
theorem
:: CLVECT_3:36
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
(
Partial_Sums
||.
seq
.||
)
.
n
>=
0
proof
end;
theorem
Th37
:
:: CLVECT_3:37
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
||.
(
(
Partial_Sums
seq
)
.
n
)
.||
<=
(
Partial_Sums
||.
seq
.||
)
.
n
proof
end;
theorem
:: CLVECT_3:38
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
being
Element
of
NAT
holds
||.
(
Sum
(
seq
,
n
)
)
.||
<=
Sum
(
||.
seq
.||
,
n
)
proof
end;
theorem
Th39
:
:: CLVECT_3:39
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
,
m
being
Element
of
NAT
holds
||.
(
(
(
Partial_Sums
seq
)
.
m
)
-
(
(
Partial_Sums
seq
)
.
n
)
)
.||
<=
abs
(
(
(
Partial_Sums
||.
seq
.||
)
.
m
)
-
(
(
Partial_Sums
||.
seq
.||
)
.
n
)
)
proof
end;
theorem
Th40
:
:: CLVECT_3:40
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
,
m
being
Element
of
NAT
holds
||.
(
(
Sum
(
seq
,
m
)
)
-
(
Sum
(
seq
,
n
)
)
)
.||
<=
abs
(
(
Sum
(
||.
seq
.||
,
m
)
)
-
(
Sum
(
||.
seq
.||
,
n
)
)
)
proof
end;
theorem
:: CLVECT_3:41
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
n
,
m
being
Element
of
NAT
holds
||.
(
Sum
(
seq
,
m
,
n
)
)
.||
<=
abs
(
Sum
(
||.
seq
.||
,
m
,
n
)
)
proof
end;
theorem
:: CLVECT_3:42
for
X
being
ComplexHilbertSpace
for
seq
being
sequence
of
X
st
seq
is
absolutely_summable
holds
seq
is
summable
proof
end;
definition
let
X
be
ComplexUnitarySpace
;
let
seq
be
sequence
of
X
;
let
Cseq
be
Complex_Sequence
;
func
Cseq
*
seq
->
sequence
of
X
means
:
Def8
:
:: CLVECT_3:def 8
for
n
being
Element
of
NAT
holds
it
.
n
=
(
Cseq
.
n
)
*
(
seq
.
n
)
;
existence
ex
b
1
being
sequence
of
X
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
(
Cseq
.
n
)
*
(
seq
.
n
)
proof
end;
uniqueness
for
b
1
,
b
2
being
sequence
of
X
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
(
Cseq
.
n
)
*
(
seq
.
n
)
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
(
Cseq
.
n
)
*
(
seq
.
n
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def8
defines
*
CLVECT_3:def 8 :
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
for
b
4
being
sequence
of
X
holds
(
b
4
=
Cseq
*
seq
iff for
n
being
Element
of
NAT
holds
b
4
.
n
=
(
Cseq
.
n
)
*
(
seq
.
n
)
);
theorem
:: CLVECT_3:43
for
X
being
ComplexUnitarySpace
for
seq1
,
seq2
being
sequence
of
X
for
Cseq
being
Complex_Sequence
holds
Cseq
*
(
seq1
+
seq2
)
=
(
Cseq
*
seq1
)
+
(
Cseq
*
seq2
)
proof
end;
theorem
:: CLVECT_3:44
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq1
,
Cseq2
being
Complex_Sequence
holds
(
Cseq1
+
Cseq2
)
*
seq
=
(
Cseq1
*
seq
)
+
(
Cseq2
*
seq
)
proof
end;
theorem
:: CLVECT_3:45
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq1
,
Cseq2
being
Complex_Sequence
holds
(
Cseq1
(#)
Cseq2
)
*
seq
=
Cseq1
*
(
Cseq2
*
seq
)
proof
end;
theorem
Th46
:
:: CLVECT_3:46
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
for
z
being
Complex
holds
(
z
(#)
Cseq
)
*
seq
=
z
*
(
Cseq
*
seq
)
proof
end;
theorem
:: CLVECT_3:47
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
holds
Cseq
*
(
-
seq
)
=
(
-
Cseq
)
*
seq
proof
end;
theorem
Th48
:
:: CLVECT_3:48
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
st
Cseq
is
convergent
&
seq
is
convergent
holds
Cseq
*
seq
is
convergent
proof
end;
theorem
:: CLVECT_3:49
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
st
Cseq
is
bounded
&
seq
is
bounded
holds
Cseq
*
seq
is
bounded
proof
end;
theorem
:: CLVECT_3:50
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
st
Cseq
is
convergent
&
seq
is
convergent
holds
(
Cseq
*
seq
is
convergent
&
lim
(
Cseq
*
seq
)
=
(
lim
Cseq
)
*
(
lim
seq
)
)
proof
end;
definition
let
Cseq
be
Complex_Sequence
;
attr
Cseq
is
Cauchy
means
:
Def9
:
:: CLVECT_3:def 9
for
r
being
Real
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
n
,
m
being
Element
of
NAT
st
n
>=
k
&
m
>=
k
holds
|.
(
(
Cseq
.
n
)
-
(
Cseq
.
m
)
)
.|
<
r
;
end;
::
deftheorem
Def9
defines
Cauchy
CLVECT_3:def 9 :
for
Cseq
being
Complex_Sequence
holds
(
Cseq
is
Cauchy
iff for
r
being
Real
st
r
>
0
holds
ex
k
being
Element
of
NAT
st
for
n
,
m
being
Element
of
NAT
st
n
>=
k
&
m
>=
k
holds
|.
(
(
Cseq
.
n
)
-
(
Cseq
.
m
)
)
.|
<
r
);
theorem
:: CLVECT_3:51
for
Cseq
being
Complex_Sequence
for
X
being
ComplexHilbertSpace
for
seq
being
sequence
of
X
st
seq
is
Cauchy
&
Cseq
is
Cauchy
holds
Cseq
*
seq
is
Cauchy
proof
end;
theorem
Th52
:
:: CLVECT_3:52
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
for
n
being
Element
of
NAT
holds
(
Partial_Sums
(
(
Cseq
-
(
Cseq
^\
1
)
)
*
(
Partial_Sums
seq
)
)
)
.
n
=
(
(
Partial_Sums
(
Cseq
*
seq
)
)
.
(
n
+
1
)
)
-
(
(
Cseq
*
(
Partial_Sums
seq
)
)
.
(
n
+
1
)
)
proof
end;
theorem
Th53
:
:: CLVECT_3:53
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
for
n
being
Element
of
NAT
holds
(
Partial_Sums
(
Cseq
*
seq
)
)
.
(
n
+
1
)
=
(
(
Cseq
*
(
Partial_Sums
seq
)
)
.
(
n
+
1
)
)
-
(
(
Partial_Sums
(
(
(
Cseq
^\
1
)
-
Cseq
)
*
(
Partial_Sums
seq
)
)
)
.
n
)
proof
end;
theorem
:: CLVECT_3:54
for
X
being
ComplexUnitarySpace
for
seq
being
sequence
of
X
for
Cseq
being
Complex_Sequence
for
n
being
Element
of
NAT
holds
Sum
(
(
Cseq
*
seq
)
,
(
n
+
1
)
)
=
(
(
Cseq
*
(
Partial_Sums
seq
)
)
.
(
n
+
1
)
)
-
(
Sum
(
(
(
(
Cseq
^\
1
)
-
Cseq
)
*
(
Partial_Sums
seq
)
)
,
n
)
)
by
Th53
;