:: CSSPACE2 semantic presentation

begin

Lm1:  for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *'
proof
let seq be Complex_Sequence; ::_thesis: Partial_Sums (seq *') = (Partial_Sums seq) *'
defpred S1[ Element of NAT ] means (Partial_Sums (seq *')) . $1 = ((Partial_Sums seq) *') . $1;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(Partial_Sums (seq *')) . (n + 1) = ((Partial_Sums (seq *')) . n) + ((seq *') . (n + 1)) by SERIES_1:def_1
.= (((Partial_Sums seq) *') . n) + ((seq . (n + 1)) *') by A2, COMSEQ_2:def_2
.= (((Partial_Sums seq) . n) *') + ((seq . (n + 1)) *') by COMSEQ_2:def_2
.= (((Partial_Sums seq) . n) + (seq . (n + 1))) *' by COMPLEX1:32
.= ((Partial_Sums seq) . (n + 1)) *' by SERIES_1:def_1 ;
hence  S1[n + 1] by COMSEQ_2:def_2; ::_thesis: verum
end;
(Partial_Sums (seq *')) . 0 = (seq *') . 0 by SERIES_1:def_1
.= (seq . 0) *' by COMSEQ_2:def_2
.= ((Partial_Sums seq) . 0) *' by SERIES_1:def_1 ;
then A3: S1[ 0 ] by COMSEQ_2:def_2;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Partial_Sums (seq *') = (Partial_Sums seq) *' by FUNCT_2:63; ::_thesis: verum
end;

Lm2:  for a, b being Real holds 0 <= (a ^2) + (b ^2)
proof
let a, b be Real; ::_thesis: 0 <= (a ^2) + (b ^2)
 ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
then  0 + 0 <= (a ^2) + (b ^2) by XREAL_1:7;
hence  0 <= (a ^2) + (b ^2) ; ::_thesis: verum
end;

Lm3:  for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.|
proof
let z1, z2 be Complex; ::_thesis: ( (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 implies |.(z1 + z2).| = |.z1.| + |.z2.| )
assume that
A1: (Re z1) * (Im z2) = (Re z2) * (Im z1) and
A2: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 ; ::_thesis: |.(z1 + z2).| = |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A3: (Re (z1 + z2)) ^2 = ((Re z1) + (Re z2)) ^2 by COMPLEX1:8
.= (((Re z1) ^2) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2) ;
 ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = abs (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) by A2, ABSVALUE:def_1;
then A4: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) = sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) by COMPLEX1:72;
A5: (Im (z1 + z2)) ^2 = ((Im z1) + (Im z2)) ^2 by COMPLEX1:8
.= (((Im z1) ^2) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2) ;
A6: 0 <= ((Re z2) ^2) + ((Im z2) ^2) by Lm2;
then A7: (sqrt (((Re z2) ^2) + ((Im z2) ^2))) ^2 = ((Re z2) ^2) + ((Im z2) ^2) by SQUARE_1:def_2;
A8: 0 <= sqrt (((Re z2) ^2) + ((Im z2) ^2)) by A6, SQUARE_1:def_2;
A9: 0 <= ((Re z1) ^2) + ((Im z1) ^2) by Lm2;
then  0 <= sqrt (((Re z1) ^2) + ((Im z1) ^2)) by SQUARE_1:def_2;
then A10: 0 + 0 <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A8, XREAL_1:7;
 ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (((Re z1) * (Im z2)) - ((Im z1) * (Re z2))) ^2 ;
then  sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = sqrt ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) by A1, XCMPLX_1:15;
then A11: sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A9, A6, SQUARE_1:29;
 (sqrt (((Re z1) ^2) + ((Im z1) ^2))) ^2 = ((Re z1) ^2) + ((Im z1) ^2) by A9, SQUARE_1:def_2;
then  sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = sqrt (((sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) ^2) by A7, A3, A5, A4, A11;
then  sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A10, SQUARE_1:22;
then  sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = (sqrt (((Re z1) ^2) + ((Im z1) ^2))) + |.z2.| by COMPLEX1:def_12;
then  sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) = |.z1.| + |.z2.| by COMPLEX1:def_12;
hence  |.(z1 + z2).| = |.z1.| + |.z2.| by COMPLEX1:def_12; ::_thesis: verum
end;

Lm4:  for seq being Complex_Sequence
for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
proof
let seq be Complex_Sequence; ::_thesis: for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
let n be Element of NAT ; ::_thesis: ( ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) implies |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n )
defpred S1[ Element of NAT ] means |.(Partial_Sums seq).| . $1 = (Partial_Sums |.seq.|) . $1;
assume A1: for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ; ::_thesis: |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n
A2: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
thus  S1[m + 1] ::_thesis: verum
proof
 for i being Element of NAT holds (Partial_Sums (Re seq)) . i >= 0
proof
defpred S2[ Element of NAT ] means (Partial_Sums (Re seq)) . $1 >= 0 ;
let i be Element of NAT ; ::_thesis: (Partial_Sums (Re seq)) . i >= 0
A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A5: S2[k] ; ::_thesis: S2[k + 1]
 ( (Partial_Sums (Re seq)) . (k + 1) = ((Partial_Sums (Re seq)) . k) + ((Re seq) . (k + 1)) & (Re seq) . (k + 1) >= 0 ) by A1, SERIES_1:def_1;
then  (Partial_Sums (Re seq)) . (k + 1) >= 0 + 0 by A5, XREAL_1:7;
hence  S2[k + 1] ; ::_thesis: verum
end;
 (Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def_1;
then A6: S2[ 0 ] by A1;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A6, A4);
hence  (Partial_Sums (Re seq)) . i >= 0 ; ::_thesis: verum
end;
then  (Partial_Sums (Re seq)) . m >= 0 ;
then  (Re (Partial_Sums seq)) . m >= 0 by COMSEQ_3:26;
then A7: Re ((Partial_Sums seq) . m) >= 0 by COMSEQ_3:def_5;
set z2 = seq . (m + 1);
set z1 = (Partial_Sums seq) . m;
A8: |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . (m + 1)).| by VALUED_1:18
.= |.(((Partial_Sums seq) . m) + (seq . (m + 1))).| by SERIES_1:def_1 ;
 for i being Element of NAT holds (Partial_Sums (Im seq)) . i = 0
proof
defpred S2[ Element of NAT ] means (Partial_Sums (Im seq)) . $1 = 0 ;
let i be Element of NAT ; ::_thesis: (Partial_Sums (Im seq)) . i = 0
A9: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
A10: (Partial_Sums (Im seq)) . (k + 1) = ((Partial_Sums (Im seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def_1;
assume  S2[k] ; ::_thesis: S2[k + 1]
hence  S2[k + 1] by A1, A10; ::_thesis: verum
end;
 (Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def_1;
then A11: S2[ 0 ] by A1;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A11, A9);
hence  (Partial_Sums (Im seq)) . i = 0 ; ::_thesis: verum
end;
then  (Partial_Sums (Im seq)) . m = 0 ;
then  (Im (Partial_Sums seq)) . m = 0 by COMSEQ_3:26;
then A12: Im ((Partial_Sums seq) . m) = 0 by COMSEQ_3:def_6;
 (Im seq) . (m + 1) = 0 by A1;
then  Im (seq . (m + 1)) = 0 by COMSEQ_3:def_6;
then A13: (Re ((Partial_Sums seq) . m)) * (Im (seq . (m + 1))) = (Re (seq . (m + 1))) * (Im ((Partial_Sums seq) . m)) by A12;
 (Re seq) . (m + 1) >= 0 by A1;
then  Re (seq . (m + 1)) >= 0 by COMSEQ_3:def_5;
then  ((Re ((Partial_Sums seq) . m)) * (Re (seq . (m + 1)))) + ((Im ((Partial_Sums seq) . m)) * (Im (seq . (m + 1)))) >= 0 by A7, A12, XREAL_1:127;
then |.(Partial_Sums seq).| . (m + 1) = |.((Partial_Sums seq) . m).| + |.(seq . (m + 1)).| by A8, A13, Lm3
.= (|.(Partial_Sums seq).| . m) + |.(seq . (m + 1)).| by VALUED_1:18
.= ((Partial_Sums |.seq.|) . m) + (|.seq.| . (m + 1)) by A3, VALUED_1:18 ;
hence  S1[m + 1] by SERIES_1:def_1; ::_thesis: verum
end;
end;
|.(Partial_Sums seq).| . 0 = |.((Partial_Sums seq) . 0).| by VALUED_1:18
.= |.(seq . 0).| by SERIES_1:def_1
.= |.seq.| . 0 by VALUED_1:18 ;
then A14: S1[ 0 ] by SERIES_1:def_1;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A14, A2);
hence  |.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n ; ::_thesis: verum
end;

Lm5:  for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *'
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable implies Sum (seq *') = (Sum seq) *' )
assume A1: seq is summable ; ::_thesis: Sum (seq *') = (Sum seq) *'
Sum (seq *') = lim (Partial_Sums (seq *')) by COMSEQ_3:def_7
.= lim ((Partial_Sums seq) *') by Lm1
.= (lim (Partial_Sums seq)) *' by A1, COMSEQ_2:12 ;
hence  Sum (seq *') = (Sum seq) *' by COMSEQ_3:def_7; ::_thesis: verum
end;

Lm6:  for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.|
proof
let seq be Complex_Sequence; ::_thesis: ( seq is absolutely_summable implies |.(Sum seq).| <= Sum |.seq.| )
A1: for k being Element of NAT holds |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k
proof
let k be Element of NAT ; ::_thesis: |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k
 |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k by COMSEQ_3:30;
hence  |.(Partial_Sums seq).| . k <= (Partial_Sums |.seq.|) . k by VALUED_1:18; ::_thesis: verum
end;
assume A2: seq is absolutely_summable ; ::_thesis: |.(Sum seq).| <= Sum |.seq.|
then reconsider Pseq = Partial_Sums seq as convergent Complex_Sequence ;
A3: |.(Sum seq).| = |.(lim (Partial_Sums seq)).| by COMSEQ_3:def_7
.= lim |.(Partial_Sums seq).| by A2, SEQ_2:27 ;
 ( |.Pseq.| is convergent & Partial_Sums |.seq.| is convergent ) by A2, SERIES_1:def_2;
then  lim |.(Partial_Sums seq).| <= lim (Partial_Sums |.seq.|) by A1, SEQ_2:18;
hence  |.(Sum seq).| <= Sum |.seq.| by A3, SERIES_1:def_3; ::_thesis: verum
end;

Lm7:  for seq being Complex_Sequence st seq is summable & ( for n being Element of NAT holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.|
proof
let seq be Complex_Sequence; ::_thesis: ( seq is summable & ( for n being Element of NAT holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) implies |.(Sum seq).| = Sum |.seq.| )
assume that
A1: seq is summable and
A2: for n being Element of NAT holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ; ::_thesis: |.(Sum seq).| = Sum |.seq.|
 for x being set st x in NAT holds
|.(Partial_Sums seq).| . x = (Partial_Sums |.seq.|) . x by A2, Lm4;
then  |.(Partial_Sums seq).| = Partial_Sums |.seq.| by FUNCT_2:12;
then  lim |.(Partial_Sums seq).| = Sum |.seq.| by SERIES_1:def_3;
then  |.(lim (Partial_Sums seq)).| = Sum |.seq.| by A1, SEQ_2:27;
hence  |.(Sum seq).| = Sum |.seq.| by COMSEQ_3:def_7; ::_thesis: verum
end;

Lm8:  for seq being Complex_Sequence
for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
proof
let seq be Complex_Sequence; ::_thesis: for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
let n be Element of NAT ; ::_thesis: ( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 )
reconsider z1 = seq . n as Element of COMPLEX ;
A1: ( 0 <= (Re z1) ^2 & 0 <= (Im z1) ^2 ) by XREAL_1:63;
(Re (seq (#) (seq *'))) . n = Re ((seq (#) (seq *')) . n) by COMSEQ_3:def_5
.= Re ((seq . n) * ((seq *') . n)) by VALUED_1:5
.= Re ((seq . n) * ((seq . n) *')) by COMSEQ_2:def_2
.= ((Re z1) ^2) + ((Im z1) ^2) by COMPLEX1:40 ;
then  (Re (seq (#) (seq *'))) . n >= 0 + 0 by A1, XREAL_1:7;
hence  (Re (seq (#) (seq *'))) . n >= 0 ; ::_thesis: (Im (seq (#) (seq *'))) . n = 0
(Im (seq (#) (seq *'))) . n = Im ((seq (#) (seq *')) . n) by COMSEQ_3:def_6
.= Im ((seq . n) * ((seq *') . n)) by VALUED_1:5
.= Im ((seq . n) * ((seq . n) *')) by COMSEQ_2:def_2 ;
hence  (Im (seq (#) (seq *'))) . n = 0 by COMPLEX1:40; ::_thesis: verum
end;

Lm9:  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
proof
 for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
proof
let x be set ; ::_thesis: ( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) )
 ( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by CSSPACE:def_1;
hence  ( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) by CSSPACE:def_11, CSSPACE:def_18; ::_thesis: verum
end;
hence  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ; ::_thesis: verum
end;

Lm10:  0. Complex_l2_Space = CZeroseq
proof
thus  0. Complex_l2_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:12, CSSPACE:def_10, CSSPACE:def_18
.= CZeroseq by CSSPACE:def_7 ; ::_thesis: verum
end;

Lm11:  for u being VECTOR of Complex_l2_Space holds u = seq_id u
proof
let u be VECTOR of Complex_l2_Space; ::_thesis: u = seq_id u
 u is VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13, CSSPACE:def_18;
hence  u = seq_id u by CSSPACE:15; ::_thesis: verum
end;

Lm12:  for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v)
proof
set W = the_set_of_l2ComplexSequences ;
set L1 = Linear_Space_of_ComplexSequences ;
let u, v be VECTOR of Complex_l2_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13, CSSPACE:def_18;
 dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A1: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) = [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) . [u,v] by CSSPACE:12, CSSPACE:def_8, CSSPACE:def_18
.= u1 + v1 by A1, CSSPACE:def_18, FUNCT_1:47 ;
hence  u + v = (seq_id u) + (seq_id v) by CSSPACE:15; ::_thesis: verum
end;

Lm13:  for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
proof
set W = the_set_of_l2ComplexSequences ;
set L1 = Linear_Space_of_ComplexSequences ;
let r be Complex; ::_thesis: for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of Complex_l2_Space; ::_thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13, CSSPACE:def_18;
 dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A1: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) = [:COMPLEX,the_set_of_l2ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
reconsider r = r as Element of COMPLEX by XCMPLX_0:def_2;
r * u = the Mult of Complex_l2_Space . [r,u] by CLVECT_1:def_1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) . [r,u] by CSSPACE:12, CSSPACE:def_9, CSSPACE:def_18
.= the Mult of Linear_Space_of_ComplexSequences . [r,u] by A1, CSSPACE:def_18, FUNCT_1:47
.= r * u1 by CLVECT_1:def_1 ;
hence  r * u = r (#) (seq_id u) by CSSPACE:15; ::_thesis: verum
end;

Lm14:  for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of Complex_l2_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r) * u by CLVECT_1:3
.= (- 1r) (#) (seq_id u) by Lm13
.= - (seq_id u) by COMSEQ_1:11 ;
hence  ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by Lm11; ::_thesis: verum
end;

Lm15:  for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of Complex_l2_Space; ::_thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by Lm12
.= (seq_id u) - (seq_id v) by Lm14 ; ::_thesis: verum
end;

Lm16:  for v, w being VECTOR of Complex_l2_Space holds |.(seq_id v).| (#) |.(seq_id w).| is summable
proof
set q0 = 1 / 2;
let u, v be VECTOR of Complex_l2_Space; ::_thesis: |.(seq_id u).| (#) |.(seq_id v).| is summable
set p = |.(seq_id v).| (#) |.(seq_id v).|;
set q = |.(seq_id u).| (#) |.(seq_id u).|;
set r = abs (|.(seq_id u).| (#) |.(seq_id v).|);
A1: for n being Element of NAT holds 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n
proof
set rr = |.(seq_id u).| (#) |.(seq_id v).|;
let n be Element of NAT ; ::_thesis: 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n
reconsider tt = abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n) as Real ;
A2: 0 <= tt by COMPLEX1:46;
(2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n = 2 * ((abs (|.(seq_id u).| (#) |.(seq_id v).|)) . n) by SEQ_1:9
.= 2 * (abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n)) by SEQ_1:12 ;
hence  0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n by A2, XREAL_1:127; ::_thesis: verum
end;
A3: for n being Element of NAT holds (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n <= ((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n
proof
set s = seq_id v;
set t = seq_id u;
let n be Element of NAT ; ::_thesis: (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n <= ((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n
reconsider sn = |.((seq_id v) . n).|, tn = |.((seq_id u) . n).| as Real ;
reconsider ss = abs sn, tt = abs tn as Real ;
A4: ((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n = ((|.(seq_id v).| (#) |.(seq_id v).|) . n) + ((|.(seq_id u).| (#) |.(seq_id u).|) . n) by SEQ_1:7
.= ((|.(seq_id v).| . n) * (|.(seq_id v).| . n)) + ((|.(seq_id u).| (#) |.(seq_id u).|) . n) by SEQ_1:8
.= ((|.(seq_id v).| . n) * (|.(seq_id v).| . n)) + ((|.(seq_id u).| . n) * (|.(seq_id u).| . n)) by SEQ_1:8
.= (|.((seq_id v) . n).| * (|.(seq_id v).| . n)) + ((|.(seq_id u).| . n) * (|.(seq_id u).| . n)) by VALUED_1:18
.= (sn ^2) + ((|.(seq_id u).| . n) * (|.(seq_id u).| . n)) by VALUED_1:18
.= (sn ^2) + (|.((seq_id u) . n).| * (|.(seq_id u).| . n)) by VALUED_1:18
.= ((abs sn) ^2) + ((abs tn) ^2) by VALUED_1:18 ;
A5: 0 <= ((abs sn) - (abs tn)) ^2 by XREAL_1:63;
(2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n = 2 * ((abs (|.(seq_id u).| (#) |.(seq_id v).|)) . n) by SEQ_1:9
.= 2 * (abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n)) by SEQ_1:12
.= 2 * (abs ((|.(seq_id u).| . n) * (|.(seq_id v).| . n))) by SEQ_1:8
.= 2 * ((abs (|.(seq_id u).| . n)) * (abs (|.(seq_id v).| . n))) by COMPLEX1:65
.= 2 * ((abs |.((seq_id u) . n).|) * (abs (|.(seq_id v).| . n))) by VALUED_1:18
.= 2 * (ss * tt) by VALUED_1:18
.= (2 * (abs sn)) * (abs tn) ;
then  0 + ((2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n) <= ((((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n) - ((2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n)) + ((2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n) by A4, A5, XREAL_1:7;
hence  (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n <= ((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n ; ::_thesis: verum
end;
A6: (1 / 2) (#) (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) = ((1 / 2) * 2) (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|)) by SEQ_1:23
.= abs (|.(seq_id u).| (#) |.(seq_id v).|) by SEQ_1:27 ;
 ( |.(seq_id v).| (#) |.(seq_id v).| is summable & |.(seq_id u).| (#) |.(seq_id u).| is summable ) by CSSPACE:def_11, CSSPACE:def_18;
then  (|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|) is summable by SERIES_1:7;
then  2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|)) is summable by A1, A3, SERIES_1:20;
then  abs (|.(seq_id u).| (#) |.(seq_id v).|) is summable by A6, SERIES_1:10;
then  |.(seq_id u).| (#) |.(seq_id v).| is absolutely_summable by SERIES_1:def_4;
hence  |.(seq_id u).| (#) |.(seq_id v).| is summable ; ::_thesis: verum
end;

Lm17:  for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *'))
proof
let v, w be VECTOR of Complex_l2_Space; ::_thesis: v .|. w = Sum ((seq_id v) (#) ((seq_id w) *'))
thus v .|. w = the scalar of Complex_l2_Space . (v,w) by CSSPACE:def_12
.= Sum ((seq_id v) (#) ((seq_id w) *')) by CSSPACE:def_17, CSSPACE:def_18 ; ::_thesis: verum
end;

Lm18:  for seq being Complex_Sequence holds |.seq.| = |.(seq *').|
proof
let seq be Complex_Sequence; ::_thesis: |.seq.| = |.(seq *').|
reconsider rseq1 = |.seq.| as Real_Sequence ;
reconsider rseq2 = |.(seq *').| as Real_Sequence ;
 for n being Element of NAT holds |.seq.| . n = |.(seq *').| . n
proof
let n be Element of NAT ; ::_thesis: |.seq.| . n = |.(seq *').| . n
|.(seq *').| . n = |.((seq *') . n).| by VALUED_1:18
.= |.((seq . n) *').| by COMSEQ_2:def_2
.= |.(seq . n).| by COMPLEX1:53 ;
hence  |.seq.| . n = |.(seq *').| . n by VALUED_1:18; ::_thesis: verum
end;
then  for n being set st n in NAT holds
rseq1 . n = rseq2 . n ;
hence  |.seq.| = |.(seq *').| by FUNCT_2:12; ::_thesis: verum
end;

Lm19:  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) )
proof
A1: for x being set st x is Element of Complex_l2_Space holds
( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable )
proof
let x be set ; ::_thesis: ( x is Element of Complex_l2_Space implies ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) )
A2: |.(seq_id x).| = |.((seq_id x) *').| by Lm18;
assume A3: x is Element of Complex_l2_Space ; ::_thesis: ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable )
then  x in the_set_of_ComplexSequences by CSSPACE:def_11, CSSPACE:def_18;
hence  x is Complex_Sequence by CSSPACE:def_1; ::_thesis: (seq_id x) (#) ((seq_id x) *') is absolutely_summable
 |.(seq_id x).| (#) |.(seq_id x).| is summable by A3, Lm16;
then  |.((seq_id x) (#) ((seq_id x) *')).| is summable by A2, COMSEQ_1:46;
hence  (seq_id x) (#) ((seq_id x) *') is absolutely_summable by COMSEQ_3:def_9; ::_thesis: verum
end;
 for x being set st x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable holds
x is Element of Complex_l2_Space
proof
let x be set ; ::_thesis: ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable implies x is Element of Complex_l2_Space )
assume that
A4: x is Complex_Sequence and
A5: (seq_id x) (#) ((seq_id x) *') is absolutely_summable ; ::_thesis: x is Element of Complex_l2_Space
 |.((seq_id x) (#) ((seq_id x) *')).| is summable by A5;
then  |.(seq_id x).| (#) |.((seq_id x) *').| is summable by COMSEQ_1:46;
then A6: |.(seq_id x).| (#) |.(seq_id x).| is summable by Lm18;
 x in the_set_of_ComplexSequences by A4, CSSPACE:def_1;
hence  x is Element of Complex_l2_Space by A6, CSSPACE:def_11, CSSPACE:def_18; ::_thesis: verum
end;
hence  for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) ) by A1; ::_thesis: verum
end;

theorem :: CSSPACE2:1
( the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) ) ) & 0. Complex_l2_Space = CZeroseq & ( for u being VECTOR of Complex_l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of Complex_l2_Space holds
( |.(seq_id v).| (#) |.(seq_id w).| is summable & ( for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *')) ) ) ) ) by Lm9, Lm10, Lm11, Lm12, Lm13, Lm14, Lm15, Lm16, Lm17, Lm19, CSSPACE:def_18;

theorem Th2: :: CSSPACE2:2
for x, y, z being Point of Complex_l2_Space
for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
proof
let x, y, z be Point of Complex_l2_Space; ::_thesis: for a being Complex holds
( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Complex; ::_thesis: ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
set seqx = seq_id x;
A1: x .|. x = the scalar of Complex_l2_Space . (x,x) by CSSPACE:def_12
.= Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def_17, CSSPACE:def_18 ;
A2: (seq_id x) (#) ((seq_id x) *') is absolutely_summable by Lm19;
then  Sum ((seq_id x) (#) ((seq_id x) *')) = (Sum (Re ((seq_id x) (#) ((seq_id x) *')))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *')))) * <i>) by COMSEQ_3:53;
then A3: ( Re (x .|. x) = Sum (Re ((seq_id x) (#) ((seq_id x) *'))) & Im (x .|. x) = Sum (Im ((seq_id x) (#) ((seq_id x) *'))) ) by A1, COMPLEX1:12;
A4: now__::_thesis:_(_x_.|._x_=_0_implies_x_=_0._Complex_l2_Space_)
set seq = seq_id x;
A5: x .|. x = the scalar of Complex_l2_Space . (x,x) by CSSPACE:def_12
.= Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def_17, CSSPACE:def_18 ;
set rseq = Re ((seq_id x) (#) ((seq_id x) *'));
A6: for n being Element of NAT holds (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2)
proof
let n be Element of NAT ; ::_thesis: (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2)
(Re ((seq_id x) (#) ((seq_id x) *'))) . n = (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) - ((Im (seq_id x)) (#) (Im ((seq_id x) *')))) . n by COMSEQ_3:21
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) + ((- ((Im (seq_id x)) (#) (Im ((seq_id x) *')))) . n) by SEQ_1:7
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) + (- (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n)) by SEQ_1:10
.= (((Re (seq_id x)) (#) (Re ((seq_id x) *'))) . n) - (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n)
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) (#) (Im ((seq_id x) *'))) . n) by SEQ_1:8
.= (((Re (seq_id x)) . n) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by SEQ_1:8
.= ((Re ((seq_id x) . n)) * ((Re ((seq_id x) *')) . n)) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def_5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - (((Im (seq_id x)) . n) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def_5
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - ((Im ((seq_id x) . n)) * ((Im ((seq_id x) *')) . n)) by COMSEQ_3:def_6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) *') . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *') . n))) by COMSEQ_3:def_6
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *'))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) *') . n))) by COMSEQ_2:def_2
.= ((Re ((seq_id x) . n)) * (Re (((seq_id x) . n) *'))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *'))) by COMSEQ_2:def_2
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (Im (((seq_id x) . n) *'))) by COMPLEX1:27
.= ((Re ((seq_id x) . n)) * (Re ((seq_id x) . n))) - ((Im ((seq_id x) . n)) * (- (Im ((seq_id x) . n)))) by COMPLEX1:27
.= ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) * (Im ((seq_id x) . n))) ;
hence  (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) ; ::_thesis: verum
end;
A7: for n being Element of NAT holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
A8: (Im ((seq_id x) . n)) ^2 >= 0 by XREAL_1:63;
 ( (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) & (Re ((seq_id x) . n)) ^2 >= 0 ) by A6, XREAL_1:63;
then  (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A8, XREAL_1:7;
hence  0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n ; ::_thesis: verum
end;
A9: (seq_id x) (#) ((seq_id x) *') is absolutely_summable by Lm19;
assume  x .|. x = 0 ; ::_thesis: x = 0. Complex_l2_Space
then  (Sum (Re ((seq_id x) (#) ((seq_id x) *')))) + ((Sum (Im ((seq_id x) (#) ((seq_id x) *')))) * <i>) = 0 by A5, A9, COMSEQ_3:53;
then A10: Sum (Re ((seq_id x) (#) ((seq_id x) *'))) = 0 by COMPLEX1:4, COMPLEX1:12;
A11: for n being Element of NAT holds (seq_id x) . n = 0
proof
let n be Element of NAT ; ::_thesis: (seq_id x) . n = 0
 (Re ((seq_id x) (#) ((seq_id x) *'))) . n = ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) by A6;
then  ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) = 0 by A9, A10, A7, RSSPACE:17;
hence  (seq_id x) . n = 0 by COMPLEX1:5; ::_thesis: verum
end;
 x is Element of the_set_of_ComplexSequences by CSSPACE:def_11, CSSPACE:def_18;
hence  x = 0. Complex_l2_Space by A11, Lm10, CSSPACE:def_6; ::_thesis: verum
end;
A12: now__::_thesis:_(_x_=_0._Complex_l2_Space_implies_x_.|._x_=_0_)
assume A13: x = 0. Complex_l2_Space ; ::_thesis: x .|. x = 0
A14: for n being Element of NAT holds ((seq_id x) (#) ((seq_id x) *')) . n = 0
proof
let n be Element of NAT ; ::_thesis: ((seq_id x) (#) ((seq_id x) *')) . n = 0
thus ((seq_id x) (#) ((seq_id x) *')) . n = ((seq_id x) . n) * (((seq_id x) *') . n) by VALUED_1:5
.= 0c * (((seq_id x) *') . n) by A13, Lm10, CSSPACE:def_6
.= 0 ; ::_thesis: verum
end;
thus x .|. x = the scalar of Complex_l2_Space . (x,x) by CSSPACE:def_12
.= Sum ((seq_id x) (#) ((seq_id x) *')) by CSSPACE:def_17, CSSPACE:def_18
.= 0 by A14, CSSPACE:80 ; ::_thesis: verum
end;
set seqy = seq_id y;
A15: for n being Element of NAT holds 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n
A16: ( (Re ((seq_id x) . n)) ^2 >= 0 & (Im ((seq_id x) . n)) ^2 >= 0 ) by XREAL_1:63;
(Re ((seq_id x) (#) ((seq_id x) *'))) . n = Re (((seq_id x) (#) ((seq_id x) *')) . n) by COMSEQ_3:def_5
.= Re (((seq_id x) . n) * (((seq_id x) *') . n)) by VALUED_1:5
.= Re (((seq_id x) . n) * (((seq_id x) . n) *')) by COMSEQ_2:def_2
.= ((Re ((seq_id x) . n)) ^2) + ((Im ((seq_id x) . n)) ^2) by COMPLEX1:40 ;
then  (Re ((seq_id x) (#) ((seq_id x) *'))) . n >= 0 + 0 by A16, XREAL_1:7;
hence  0 <= (Re ((seq_id x) (#) ((seq_id x) *'))) . n ; ::_thesis: verum
end;
 |.(seq_id x).| (#) |.(seq_id y).| is summable by Lm16;
then  |.((seq_id x) *').| (#) |.(seq_id y).| is summable by Lm18;
then  |.(((seq_id x) *') (#) (seq_id y)).| is summable by COMSEQ_1:46;
then A17: ((seq_id x) *') (#) (seq_id y) is absolutely_summable by COMSEQ_3:def_9;
set seqz = seq_id z;
A18: for n being Element of NAT holds (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0
proof
let n be Element of NAT ; ::_thesis: (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0
(Im ((seq_id x) (#) ((seq_id x) *'))) . n = Im (((seq_id x) (#) ((seq_id x) *')) . n) by COMSEQ_3:def_6
.= Im (((seq_id x) . n) * (((seq_id x) *') . n)) by VALUED_1:5
.= Im (((seq_id x) . n) * (((seq_id x) . n) *')) by COMSEQ_2:def_2 ;
hence  (Im ((seq_id x) (#) ((seq_id x) *'))) . n = 0 by COMPLEX1:40; ::_thesis: verum
end;
 |.(seq_id x).| (#) |.(seq_id z).| is summable by Lm16;
then  |.(seq_id x).| (#) |.((seq_id z) *').| is summable by Lm18;
then  |.((seq_id x) (#) ((seq_id z) *')).| is summable by COMSEQ_1:46;
then A19: (seq_id x) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def_9;
 |.(seq_id y).| (#) |.(seq_id z).| is summable by Lm16;
then  |.(seq_id y).| (#) |.((seq_id z) *').| is summable by Lm18;
then  |.((seq_id y) (#) ((seq_id z) *')).| is summable by COMSEQ_1:46;
then A20: (seq_id y) (#) ((seq_id z) *') is absolutely_summable by COMSEQ_3:def_9;
A21: (x + y) .|. z = the scalar of Complex_l2_Space . ((x + y),z) by CSSPACE:def_12
.= Sum ((seq_id (x + y)) (#) ((seq_id z) *')) by CSSPACE:def_17, CSSPACE:def_18
.= Sum ((seq_id ((seq_id x) + (seq_id y))) (#) ((seq_id z) *')) by Lm12
.= Sum (((seq_id x) + (seq_id y)) (#) ((seq_id z) *')) by CSSPACE:1
.= Sum (((seq_id x) (#) ((seq_id z) *')) + ((seq_id y) (#) ((seq_id z) *'))) by COMSEQ_1:10
.= (Sum ((seq_id x) (#) ((seq_id z) *'))) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by A19, A20, COMSEQ_3:54
.= ( the scalar of Complex_l2_Space . (x,z)) + (Sum ((seq_id y) (#) ((seq_id z) *'))) by CSSPACE:def_17, CSSPACE:def_18
.= ( the scalar of Complex_l2_Space . (x,z)) + ( the scalar of Complex_l2_Space . (y,z)) by CSSPACE:def_17, CSSPACE:def_18
.= (x .|. z) + ( the scalar of Complex_l2_Space . (y,z)) by CSSPACE:def_12
.= (x .|. z) + (y .|. z) by CSSPACE:def_12 ;
 |.(seq_id x).| (#) |.(seq_id y).| is summable by Lm16;
then  |.(seq_id x).| (#) |.((seq_id y) *').| is summable by Lm18;
then  |.((seq_id x) (#) ((seq_id y) *')).| is summable by COMSEQ_1:46;
then A22: (seq_id x) (#) ((seq_id y) *') is absolutely_summable by COMSEQ_3:def_9;
A23: a in COMPLEX by XCMPLX_0:def_2;
A24: (a * x) .|. y = the scalar of Complex_l2_Space . ((a * x),y) by CSSPACE:def_12
.= Sum ((seq_id (a * x)) (#) ((seq_id y) *')) by CSSPACE:def_17, CSSPACE:def_18
.= Sum ((seq_id (a (#) (seq_id x))) (#) ((seq_id y) *')) by Lm13
.= Sum ((a (#) (seq_id x)) (#) ((seq_id y) *')) by CSSPACE:1
.= Sum (a (#) ((seq_id x) (#) ((seq_id y) *'))) by A23, COMSEQ_1:12
.= a * (Sum ((seq_id x) (#) ((seq_id y) *'))) by A22, COMSEQ_3:56
.= a * ( the scalar of Complex_l2_Space . (x,y)) by CSSPACE:def_17, CSSPACE:def_18
.= a * (x .|. y) by CSSPACE:def_12 ;
x .|. y = the scalar of Complex_l2_Space . (x,y) by CSSPACE:def_12
.= Sum ((seq_id x) (#) ((seq_id y) *')) by CSSPACE:def_17, CSSPACE:def_18
.= Sum ((((seq_id x) *') *') (#) ((seq_id y) *'))
.= Sum ((((seq_id x) *') (#) (seq_id y)) *') by COMSEQ_2:5
.= (Sum (((seq_id x) *') (#) (seq_id y))) *' by A17, Lm5
.= ( the scalar of Complex_l2_Space . (y,x)) *' by CSSPACE:def_17, CSSPACE:def_18
.= (y .|. x) *' by CSSPACE:def_12 ;
hence  ( ( x .|. x = 0 implies x = 0. Complex_l2_Space ) & ( x = 0. Complex_l2_Space implies x .|. x = 0 ) & Re (x .|. x) >= 0 & Im (x .|. x) = 0 & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) by A4, A12, A2, A3, A15, A18, A21, A24, RSSPACE:16, SERIES_1:18; ::_thesis: verum
end;

registration
cluster Complex_l2_Space  ->  ComplexUnitarySpace-like ;
coherence
 Complex_l2_Space is ComplexUnitarySpace-like by Th2, CSSPACE:def_13;
end;

Lm20:  for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2)
proof
let x, y be Complex; ::_thesis: 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2)
set a = |.x.|;
set b = |.y.|;
 (|.x.| - |.y.|) ^2 = ((|.x.| * |.x.|) - ((|.x.| * |.y.|) + (|.x.| * |.y.|))) + (|.y.| * |.y.|) ;
then  ( |.x.| * |.y.| = |.(x * y).| & ((|.x.| * |.x.|) + (|.y.| * |.y.|)) - ((|.x.| * |.y.|) + (|.x.| * |.y.|)) >= 0 ) by COMPLEX1:65, XREAL_1:63;
hence  2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by XREAL_1:49; ::_thesis: verum
end;

Lm21:  for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) )
proof
A1: now__::_thesis:_for_x,_y_being_Complex_holds_|.(x_+_y).|_*_|.(x_+_y).|_<=_((2_*_|.x.|)_*_|.x.|)_+_((2_*_|.y.|)_*_|.y.|)
let x, y be Complex; ::_thesis: |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|)
A2: ( |.(x * x).| = |.x.| * |.x.| & |.(y * y).| = |.y.| * |.y.| ) by COMPLEX1:65;
 |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| <= |.(((x * x) + (x * y)) + (x * y)).| + |.(y * y).| by COMPLEX1:56;
then A3: |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| - |.(y * y).| <= |.(((x * x) + (x * y)) + (x * y)).| by XREAL_1:20;
 |.(((x * x) + (x * y)) + (x * y)).| <= |.((x * x) + (x * y)).| + |.(x * y).| by COMPLEX1:56;
then  ( |.((x * x) + (x * y)).| <= |.(x * x).| + |.(x * y).| & |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.((x * x) + (x * y)).| ) by COMPLEX1:56, XREAL_1:20;
then  |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.(x * x).| + |.(x * y).| by XXREAL_0:2;
then A4: |.(((x * x) + (x * y)) + (x * y)).| <= (|.(x * x).| + |.(x * y).|) + |.(x * y).| by XREAL_1:20;
|.(x + y).| * |.(x + y).| = |.((x + y) * (x + y)).| by COMPLEX1:65
.= |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| ;
then  (|.(x + y).| * |.(x + y).|) - |.(y * y).| <= |.(x * x).| + (2 * |.(x * y).|) by A3, A4, XXREAL_0:2;
then A5: ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= 2 * |.(x * y).| by XREAL_1:20;
 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by Lm20;
then  ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= (|.x.| ^2) + (|.y.| ^2) by A5, XXREAL_0:2;
then  (|.(x + y).| * |.(x + y).|) - (|.y.| * |.y.|) <= ((|.x.| * |.x.|) + (|.y.| * |.y.|)) + (|.x.| * |.x.|) by A2, XREAL_1:20;
then  |.(x + y).| * |.(x + y).| <= ((2 * (|.x.| * |.x.|)) + (|.y.| * |.y.|)) + (|.y.| * |.y.|) by XREAL_1:20;
hence  |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Complex_holds_|.x.|_*_|.x.|_<=_((2_*_|.(x_-_y).|)_*_|.(x_-_y).|)_+_((2_*_|.y.|)_*_|.y.|)
let x, y be Complex; ::_thesis: |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|)
 |.((x - y) + y).| = |.x.| ;
hence  |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) by A1; ::_thesis: verum
end;
hence  for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by A1; ::_thesis: verum
end;

Lm22:  for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
proof
let c be Complex; ::_thesis: for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def_2;
reconsider cseq = NAT --> c1 as Complex_Sequence ;
A1: for n being Element of NAT holds cseq . n = c by FUNCOP_1:7;
then A2: cseq is convergent by COMSEQ_2:9;
let seq be Complex_Sequence; ::_thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) )
assume A3: seq is convergent ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
reconsider seq1 = seq - cseq as convergent Complex_Sequence by A3, A2;
 |.seq1.| is convergent ;
then A4: lim (|.(seq - cseq).| (#) |.(seq - cseq).|) = (lim |.(seq - cseq).|) * (lim |.(seq - cseq).|) by SEQ_2:15
.= |.((lim seq) - (lim cseq)).| * (lim |.(seq - cseq).|) by A3, A2, SEQ_2:31
.= |.((lim seq) - (lim cseq)).| * |.((lim seq) - (lim cseq)).| by A3, A2, SEQ_2:31
.= |.((lim seq) - c).| * |.((lim seq) - (lim cseq)).| by A1, COMSEQ_2:10
.= |.((lim seq) - c).| * |.((lim seq) - c).| by A1, COMSEQ_2:10 ;
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) )
assume A5: for i being Element of NAT holds rseq . i = |.((seq . i) - c).| * |.((seq . i) - c).| ; ::_thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| )
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_(|.(seq_-_cseq).|_(#)_|.(seq_-_cseq).|)_._i
let i be Element of NAT ; ::_thesis: rseq . i = (|.(seq - cseq).| (#) |.(seq - cseq).|) . i
thus rseq . i = |.((seq . i) - c).| * |.((seq . i) - c).| by A5
.= |.((seq . i) - (cseq . i)).| * |.((seq . i) - c).| by FUNCOP_1:7
.= |.((seq . i) - (cseq . i)).| * |.((seq . i) - (cseq . i)).| by FUNCOP_1:7
.= |.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + (- (cseq . i))).| by VALUED_1:8
.= |.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + ((- cseq) . i)).| by VALUED_1:8
.= |.((seq + (- cseq)) . i).| * |.((seq . i) + ((- cseq) . i)).| by VALUED_1:1
.= |.((seq - cseq) . i).| * |.((seq + (- cseq)) . i).| by VALUED_1:1
.= (|.(seq - cseq).| . i) * |.((seq - cseq) . i).| by VALUED_1:18
.= (|.(seq - cseq).| . i) * (|.(seq - cseq).| . i) by VALUED_1:18
.= (|.(seq - cseq).| (#) |.(seq - cseq).|) . i by SEQ_1:8 ; ::_thesis: verum
end;
then A6: for x being set st x in NAT holds
rseq . x = (|.(seq - cseq).| (#) |.(seq - cseq).|) . x ;
 |.seq1.| (#) |.seq1.| is convergent ;
hence  ( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by A6, A4, FUNCT_2:12; ::_thesis: verum
end;

Lm23:  for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
proof
let c be Complex; ::_thesis: for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
let seq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
let seq be Complex_Sequence; ::_thesis: ( seq is convergent & seq1 is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) )
assume that
A1: seq is convergent and
A2: seq1 is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def_2;
reconsider cseq = NAT --> c1 as Complex_Sequence ;
A3: for n being Element of NAT holds cseq . n = c by FUNCOP_1:7;
then A4: cseq is convergent by COMSEQ_2:9;
then reconsider s = seq - cseq as convergent Complex_Sequence by A1;
A5: |.s.| is convergent ;
then A6: |.(seq - cseq).| (#) |.(seq - cseq).| is convergent ;
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) )
assume A7: for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ; ::_thesis: ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) )
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_((|.(seq_-_cseq).|_(#)_|.(seq_-_cseq).|)_+_seq1)_._i
let i be Element of NAT ; ::_thesis: rseq . i = ((|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) . i
thus rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) by A7
.= (|.((seq . i) - (cseq . i)).| * |.((seq . i) - c).|) + (seq1 . i) by FUNCOP_1:7
.= (|.((seq . i) - (cseq . i)).| * |.((seq . i) - (cseq . i)).|) + (seq1 . i) by FUNCOP_1:7
.= (|.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + (- (cseq . i))).|) + (seq1 . i) by VALUED_1:8
.= (|.((seq . i) + ((- cseq) . i)).| * |.((seq . i) + ((- cseq) . i)).|) + (seq1 . i) by VALUED_1:8
.= (|.((seq + (- cseq)) . i).| * |.((seq . i) + ((- cseq) . i)).|) + (seq1 . i) by VALUED_1:1
.= (|.((seq - cseq) . i).| * |.((seq + (- cseq)) . i).|) + (seq1 . i) by VALUED_1:1
.= ((|.(seq - cseq).| . i) * |.((seq - cseq) . i).|) + (seq1 . i) by VALUED_1:18
.= ((|.(seq - cseq).| . i) * (|.(seq - cseq).| . i)) + (seq1 . i) by VALUED_1:18
.= ((|.(seq - cseq).| (#) |.(seq - cseq).|) . i) + (seq1 . i) by SEQ_1:8
.= ((|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1) . i by SEQ_1:7 ; ::_thesis: verum
end;
then A8: rseq = (|.(seq - cseq).| (#) |.(seq - cseq).|) + seq1 by FUNCT_2:63;
lim (|.(seq - cseq).| (#) |.(seq - cseq).|) = (lim |.(seq - cseq).|) * (lim |.(seq - cseq).|) by A5, SEQ_2:15
.= |.((lim seq) - (lim cseq)).| * (lim |.(seq - cseq).|) by A1, A4, SEQ_2:31
.= |.((lim seq) - (lim cseq)).| * |.((lim seq) - (lim cseq)).| by A1, A4, SEQ_2:31
.= |.((lim seq) - c).| * |.((lim seq) - (lim cseq)).| by A3, COMSEQ_2:10
.= |.((lim seq) - c).| * |.((lim seq) - c).| by A3, COMSEQ_2:10 ;
hence  ( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by A2, A8, A6, SEQ_2:6; ::_thesis: verum
end;

registration
cluster Complex_l2_Space  ->  complete ;
coherence
 Complex_l2_Space is complete
proof
let vseq be sequence of Complex_l2_Space; :: according to CLVECT_2:def_11 ::_thesis: ( not vseq is Cauchy or vseq is convergent )
assume A1: vseq is Cauchy ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means  ex i being Element of NAT st
( c1 = i & ex seqi being Complex_Sequence st
( ( for n being Element of NAT holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & c2 = lim seqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in COMPLEX & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( set ) ->  Element of COMPLEX = (seq_id (vseq . c1)) . i;
consider seqi being Complex_Sequence such that
A3: for n being Element of NAT holds seqi . n = H1(n) from COMSEQ_1:sch_1();
take  lim seqi ; ::_thesis: ( lim seqi in COMPLEX & S1[x, lim seqi] )
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((seqi_._m)_-_(seqi_._k)).|_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seqi . m) - (seqi . k)).| < e )
assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seqi . m) - (seqi . k)).| < e
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seqi . m) - (seqi . k)).| < e ::_thesis: verum
proof
consider k being Element of NAT  such that
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, CLVECT_2:58;
now__::_thesis:_for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((seqi_._m)_-_(seqi_._k)).|_<_e
reconsider e1 = e as Real ;
set vk = vseq . k;
let m be Element of NAT ; ::_thesis: ( k <= m implies |.((seqi . m) - (seqi . k)).| < e )
assume A6: k <= m ; ::_thesis: |.((seqi . m) - (seqi . k)).| < e
set vm = vseq . m;
 ||.((vseq . m) - (vseq . k)).|| < e by A5, A6;
then A7: sqrt |.(((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))).| < e by CSSPACE:def_15;
set seqmk = seq_id ((vseq . m) - (vseq . k));
A8: sqrt (|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) = sqrt (|.((seqi . m) - (seqi . k)).| ^2)
.= |.((seqi . m) - (seqi . k)).| by COMPLEX1:46, SQUARE_1:22 ;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Lm15
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by CSSPACE:1 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by VALUED_1:8
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (seqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (seqi . m) - (seqi . k) by A3 ;
then |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * |.((seq_id ((vseq . m) - (vseq . k))) . i).| by VALUED_1:18
.= (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i) by VALUED_1:18 ;
then  (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.((seq_id ((vseq . m) - (vseq . k))) *').| . i) = |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| by Lm18;
then A9: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i by SEQ_1:8;
 0 <= |.((seqi . m) - (seqi . k)).| by COMPLEX1:46;
then A10: 0 <= |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| by XREAL_1:127;
 ( (seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *') is absolutely_summable & ( for j being Element of NAT holds
( (Re ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))) . j >= 0 & (Im ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))) . j = 0 ) ) ) by Lm8, Lm19;
then |.(Sum ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *'))).| = Sum |.((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *')).| by Lm7
.= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) by COMSEQ_1:46 ;
then A11: sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)) < e by A7, Lm17;
A12: for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i
proof
let i be Element of NAT ; ::_thesis: 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i
(|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i = (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.((seq_id ((vseq . m) - (vseq . k))) *').| . i) by SEQ_1:8
.= (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i) by Lm18 ;
hence  0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i by XREAL_1:63; ::_thesis: verum
end;
 |.(seq_id ((vseq . m) - (vseq . k))).| (#) |.(seq_id ((vseq . m) - (vseq . k))).| is summable by CSSPACE:def_11, CSSPACE:def_18;
then A13: |.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').| is summable by Lm18;
then A14: 0 <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) by A12, SERIES_1:18;
then  0 <= sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)) by SQUARE_1:def_2;
then  (sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|))) ^2 < e1 ^2 by A11, SQUARE_1:16;
then A15: Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) < e * e by A14, SQUARE_1:def_2;
 (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) by A13, A12, RSSPACE2:3;
then A16: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| < e * e by A15, A9, XXREAL_0:2;
sqrt (e * e) = sqrt (e1 ^2)
.= e by A4, SQUARE_1:22 ;
hence  |.((seqi . m) - (seqi . k)).| < e by A10, A16, A8, SQUARE_1:27; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((seqi . m) - (seqi . k)).| < e ; ::_thesis: verum
end;
end;
then  seqi is convergent by COMSEQ_3:46;
hence  ( lim seqi in COMPLEX & S1[x, lim seqi] ) by A3; ::_thesis: verum
end;
consider f being Function of NAT,COMPLEX such that
A17: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider tseq = f as Complex_Sequence ;
set seqt = seq_id tseq;
A18: now__::_thesis:_for_i_being_Element_of_NAT_ex_seqi_being_Complex_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_seqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_seqi_is_convergent_&_tseq_._i_=_lim_seqi_)
let i be Element of NAT ; ::_thesis: ex seqi being Complex_Sequence st
( ( for n being Element of NAT holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & tseq . i = lim seqi )
reconsider x = i as set ;
 ex i0 being Element of NAT st
( x = i0 & ex seqi being Complex_Sequence st
( ( for n being Element of NAT holds seqi . n = (seq_id (vseq . n)) . i0 ) & seqi is convergent & f . x = lim seqi ) ) by A17;
hence  ex seqi being Complex_Sequence st
( ( for n being Element of NAT holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & tseq . i = lim seqi ) ; ::_thesis: verum
end;
A19: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e * e )
proof
let e1 be Real; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 ) )
assume A20: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 )
set e = e1 / 2;
A21: e1 / 2 > 0 by A20, XREAL_1:215;
then consider k being Element of NAT  such that
A22: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, CLVECT_2:58;
 e1 / 2 < e1 by A20, XREAL_1:216;
then A23: (e1 / 2) * (e1 / 2) < e1 * e1 by A21, XREAL_1:97;
A24: for m, n being Element of NAT st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )
proof
let m, n be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) )
assume  ( n >= k & m >= k ) ; ::_thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )
then  ||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A22;
then A25: sqrt |.(((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))).| < e1 / 2 by CSSPACE:def_15;
 ( (seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *') is absolutely_summable & ( for j being Element of NAT holds
( (Re ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *'))) . j >= 0 & (Im ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *'))) . j = 0 ) ) ) by Lm8, Lm19;
then |.(Sum ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *'))).| = Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *')).| by Lm7
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.((seq_id ((vseq . n) - (vseq . m))) *').|) by COMSEQ_1:46
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by Lm18
.= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:46 ;
then A26: sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) < e1 / 2 by A25, Lm17;
A27: for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i
proof
let i be Element of NAT ; ::_thesis: 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i
(|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i = |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| . i by COMSEQ_1:46
.= |.(((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i).| by VALUED_1:18 ;
hence  0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i by COMPLEX1:46; ::_thesis: verum
end;
 |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable by CSSPACE:def_11, CSSPACE:def_18;
then  0 <= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by A27, SERIES_1:18;
then A28: 0 <= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:46;
then  0 <= sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) by SQUARE_1:def_2;
then  (sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|)) ^2 < (e1 / 2) ^2 by A26, SQUARE_1:16;
then  Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| < (e1 / 2) * (e1 / 2) by A28, SQUARE_1:def_2;
hence  ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) by A27, COMSEQ_1:46, CSSPACE:def_11, CSSPACE:def_18; ::_thesis: verum
end;
A29: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i )
proof
let n be Element of NAT ; ::_thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i )
defpred S2[ Element of NAT ] means  for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . c1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . c1 );
A30: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
proof
let m, k be Element of NAT ; ::_thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
thus  seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Lm15
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by CSSPACE:1 ; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_st_(_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_(|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_(#)_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|))_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_(#)_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|))_._i_)_)_holds_
for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_(|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_(#)_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|))_._(i_+_1)_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_(#)_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|))_._(i_+_1)_)
let i be Element of NAT ; ::_thesis: ( ( for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) ) implies for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) )
assume A31: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) ; ::_thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) )
thus  for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) ::_thesis: verum
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums (|.(seq_id ((vseq . c1) - (vseq . n))).| (#) |.(seq_id ((vseq . c1) - (vseq . n))).|)) . i;
consider rseqb being Real_Sequence such that
A32: for m being Element of NAT holds rseqb . m = H1(m) from SEQ_1:sch_1();
consider seq0 being Complex_Sequence such that
A33: for m being Element of NAT holds seq0 . m = (seq_id (vseq . m)) . (i + 1) and
A34: seq0 is convergent and
A35: tseq . (i + 1) = lim seq0 by A18;
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) )
assume A36: for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) )
A37: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_(|.((seq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1))).|_*_|.((seq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1))).|)_+_(rseqb_._m)
let m be Element of NAT ; ::_thesis: rseq . m = (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m)
thus rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) by A36
.= ((|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i) by SERIES_1:def_1
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i) by A30
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + (rseqb . m) by A32
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . (i + 1)) + (rseqb . m) by A30
.= ((|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . (i + 1)) * (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . (i + 1))) + (rseqb . m) by SEQ_1:8
.= (|.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).| * (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . (i + 1))) + (rseqb . m) by VALUED_1:18
.= (|.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).|) + (rseqb . m) by VALUED_1:18
.= (|.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).|) + (rseqb . m) by VALUED_1:1
.= (|.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (rseqb . m) by VALUED_1:1
.= (|.(((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).| * |.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (rseqb . m) by VALUED_1:8
.= (|.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).|) + (rseqb . m) by VALUED_1:8
.= (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m) by A33
.= (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m) by A33 ; ::_thesis: verum
end;
A38: rseqb is convergent by A31, A32;
then  lim rseq = (|.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).| * |.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).|) + (lim rseqb) by A34, A37, Lm23
.= (|.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).|) + (lim rseqb) by A35, VALUED_1:8
.= (|.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (lim rseqb) by VALUED_1:8
.= (|.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).| * |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (lim rseqb) by VALUED_1:1
.= (|.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).| * |.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).|) + (lim rseqb) by VALUED_1:1
.= ((|.(tseq + (- (seq_id (vseq . n)))).| . (i + 1)) * |.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).|) + (lim rseqb) by VALUED_1:18
.= ((|.(tseq - (seq_id (vseq . n))).| . (i + 1)) * (|.(tseq + (- (seq_id (vseq . n)))).| . (i + 1))) + (lim rseqb) by VALUED_1:18
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . (i + 1)) + (lim rseqb) by SEQ_1:8
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by A31, A32
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by CSSPACE:1
.= ((|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by CSSPACE:1
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) by SERIES_1:def_1 ;
hence  ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) by A38, A34, A37, Lm23; ::_thesis: verum
end;
end;
then A39: for i being Element of NAT st S2[i] holds
S2[i + 1] ;
now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_(|.(seq_id_((vseq_._m)_-_(vseq_._n))).|_(#)_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|))_._0_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_(|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_(#)_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|))_._0_)
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) )
assume A40: for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 )
thus  ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) ::_thesis: verum
proof
consider rseq0 being Complex_Sequence such that
A41: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A42: rseq0 is convergent and
A43: tseq . 0 = lim rseq0 by A18;
A44: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.((rseq0_._m)_-_((seq_id_(vseq_._n))_._0)).|_*_|.((rseq0_._m)_-_((seq_id_(vseq_._n))_._0)).|
let m be Element of NAT ; ::_thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|
thus rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 by A40
.= (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 by SERIES_1:def_1
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 by A30
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . 0 by A30
.= (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . 0) * (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . 0) by SEQ_1:8
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| * (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . 0) by VALUED_1:18
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| by VALUED_1:1
.= |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| * |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:1
.= |.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))).| * |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:8
.= |.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))).| * |.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))).| by VALUED_1:8
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| * |.(((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)).| by A41
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| by A41 ; ::_thesis: verum
end;
then  lim rseq = |.((tseq . 0) - ((seq_id (vseq . n)) . 0)).| * |.((tseq . 0) - ((seq_id (vseq . n)) . 0)).| by A42, A43, Lm22
.= |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| * |.((tseq . 0) + (- ((seq_id (vseq . n)) . 0))).| by VALUED_1:8
.= |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| * |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:8
.= |.((tseq + (- (seq_id (vseq . n)))) . 0).| * |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:1
.= |.((tseq - (seq_id (vseq . n))) . 0).| * |.((tseq + (- (seq_id (vseq . n)))) . 0).| by VALUED_1:1
.= (|.(tseq - (seq_id (vseq . n))).| . 0) * |.((tseq - (seq_id (vseq . n))) . 0).| by VALUED_1:18
.= (|.(tseq - (seq_id (vseq . n))).| . 0) * (|.(tseq - (seq_id (vseq . n))).| . 0) by VALUED_1:18
.= (|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . 0 by SEQ_1:8
.= (Partial_Sums (|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|)) . 0 by SERIES_1:def_1
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|)) . 0 by CSSPACE:1
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 by CSSPACE:1 ;
hence  ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) by A42, A44, Lm22; ::_thesis: verum
end;
end;
then A45: S2[ 0 ] ;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A45, A39);
hence  for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) ; ::_thesis: verum
end;
 for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 )
proof
let n be Element of NAT ; ::_thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 ) )
assume A46: n >= k ; ::_thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 )
A47: for i being Element of NAT st 0 <= i holds
(Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2)
proof
let i be Element of NAT ; ::_thesis: ( 0 <= i implies (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) )
assume  0 <= i ; ::_thesis: (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2)
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums (|.(seq_id ((vseq . c1) - (vseq . n))).| (#) |.(seq_id ((vseq . c1) - (vseq . n))).|)) . i;
consider rseq being Real_Sequence such that
A48: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A49: for m being Element of NAT st m >= k holds
rseq . m <= (e1 / 2) * (e1 / 2)
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= (e1 / 2) * (e1 / 2) )
assume A50: m >= k ; ::_thesis: rseq . m <= (e1 / 2) * (e1 / 2)
 ( |.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).| is summable & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . i ) ) by A24, A46, A50;
then A51: (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i <= Sum (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) by RSSPACE2:3;
A52: rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i by A48;
 Sum (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) < (e1 / 2) * (e1 / 2) by A24, A46, A50;
hence  rseq . m <= (e1 / 2) * (e1 / 2) by A52, A51, XXREAL_0:2; ::_thesis: verum
end;
 ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) by A29, A48;
hence  (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) by A49, RSSPACE2:5; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_holds_(Partial_Sums_(|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|_(#)_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|))_._i_<_e1_*_e1
let i be Element of NAT ; ::_thesis: (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1
 (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) by A47, NAT_1:2;
hence  (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1 by A23, XXREAL_0:2; ::_thesis: verum
end;
then A53: Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is bounded_above by SEQ_2:def_3;
A54: for i being Element of NAT holds 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i
proof
let i be Element of NAT ; ::_thesis: 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i
 (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i = (|.((seq_id tseq) - (seq_id (vseq . n))).| . i) * (|.((seq_id tseq) - (seq_id (vseq . n))).| . i) by SEQ_1:8;
hence  0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i by XREAL_1:63; ::_thesis: verum
end;
then A55: |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable by A53, SERIES_1:17;
then  Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is convergent by SERIES_1:def_2;
then  ( Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) = lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) & lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) <= (e1 / 2) * (e1 / 2) ) by A47, RSSPACE2:5, SERIES_1:def_3;
then A56: Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) < e1 * e1 by A23, XXREAL_0:2;
 |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(((seq_id tseq) - (seq_id (vseq . n))) *').| is summable by A55, Lm18;
then  |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| is summable by COMSEQ_1:46;
then  ((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *') is absolutely_summable by COMSEQ_3:def_9;
then A57: |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| <= Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| by Lm6;
 |.((seq_id tseq) - (seq_id (vseq . n))).| = |.(((seq_id tseq) - (seq_id (vseq . n))) *').| by Lm18;
then  Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| < e1 * e1 by A56, COMSEQ_1:46;
hence  ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 ) by A54, A53, A57, SERIES_1:17, XXREAL_0:2; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e1 * e1 ) ; ::_thesis: verum
end;
A58: |.(seq_id tseq).| (#) |.(seq_id tseq).| is summable
proof
set d = |.(seq_id tseq).| (#) |.(seq_id tseq).|;
A59: for i being Element of NAT holds 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i
proof
let i be Element of NAT ; ::_thesis: 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i
 (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i = (|.(seq_id tseq).| . i) * (|.(seq_id tseq).| . i) by SEQ_1:8;
hence  0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i by XREAL_1:63; ::_thesis: verum
end;
consider m being Element of NAT  such that
A60: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < 1 * 1 ) by A19;
set b = |.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|;
 |.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).| is summable by CSSPACE:def_11, CSSPACE:def_18;
then A61: 2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) is summable by SERIES_1:10;
A62: for i being Element of NAT holds (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i
proof
let i be Element of NAT ; ::_thesis: (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i
A63: ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i = ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) . i) + ((2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) . i) by SEQ_1:7
.= (2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i)) + ((2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) . i) by SEQ_1:9
.= (2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i)) + (2 * ((|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) . i)) by SEQ_1:9 ;
set y = (seq_id (vseq . m)) . i;
set x = (seq_id tseq) . i;
A64: 2 * ((|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) . i) = 2 * ((|.(seq_id (vseq . m)).| . i) * (|.(seq_id (vseq . m)).| . i)) by SEQ_1:8
.= 2 * (|.((seq_id (vseq . m)) . i).| * (|.(seq_id (vseq . m)).| . i)) by VALUED_1:18
.= 2 * (|.((seq_id (vseq . m)) . i).| * |.((seq_id (vseq . m)) . i).|) by VALUED_1:18
.= (2 * |.((seq_id (vseq . m)) . i).|) * |.((seq_id (vseq . m)) . i).| ;
|.((seq_id tseq) - (seq_id (vseq . m))).| . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by VALUED_1:18
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by VALUED_1:1
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then  (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i = |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| by SEQ_1:8;
then A65: 2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i) = (2 * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).|) * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
(|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i = (|.(seq_id tseq).| . i) * (|.(seq_id tseq).| . i) by SEQ_1:8
.= |.((seq_id tseq) . i).| * (|.(seq_id tseq).| . i) by VALUED_1:18
.= |.((seq_id tseq) . i).| * |.((seq_id tseq) . i).| by VALUED_1:18 ;
hence  (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i by A63, A65, A64, Lm21; ::_thesis: verum
end;
 |.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).| is summable by A60;
then  2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) is summable by SERIES_1:10;
then  (2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) is summable by A61, SERIES_1:7;
hence  |.(seq_id tseq).| (#) |.(seq_id tseq).| is summable by A59, A62, SERIES_1:20; ::_thesis: verum
end;
 tseq in the_set_of_ComplexSequences by CSSPACE:def_1;
then reconsider tv = tseq as Point of Complex_l2_Space by A58, CSSPACE:def_11, CSSPACE:def_18;
 for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A66: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT  such that
A67: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e * e ) by A19, A66;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
 tseq in the_set_of_ComplexSequences by CSSPACE:def_1;
then reconsider u = tseq as VECTOR of Complex_l2_Space by A58, CSSPACE:def_11, CSSPACE:def_18;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A68: n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
reconsider v = vseq . n as VECTOR of Complex_l2_Space ;
set seqvn = seq_id (vseq . n);
 0 <= Re ((u - v) .|. (u - v)) by CSSPACE:def_13;
then A69: 0 <= |.((u - v) .|. (u - v)).| by CSSPACE:34;
 seq_id (u - v) = u - v by Lm11;
then A70: seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Lm15;
 |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e * e by A67, A68;
then  |.((u - v) .|. (u - v)).| < e * e by A70, Lm17;
then A71: sqrt |.((u - v) .|. (u - v)).| < sqrt (e ^2) by A69, SQUARE_1:27;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by CSSPACE:47
.= sqrt |.((u - v) .|. (u - v)).| by CSSPACE:def_15 ;
hence  ||.((vseq . n) - tv).|| < e by A66, A71, SQUARE_1:22; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence  vseq is convergent by CLVECT_2:9; ::_thesis: verum
end;
end;

registration
clusterV80() right_complementable V131() V132() V133() vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like complete for CUNITSTR ;
existence
 ex b1 being ComplexUnitarySpace st b1 is complete
proof
take  Complex_l2_Space ; ::_thesis: Complex_l2_Space is complete
thus  Complex_l2_Space is complete ; ::_thesis: verum
end;
end;

definition
mode ComplexHilbertSpace is complete ComplexUnitarySpace;
end;

begin

theorem :: CSSPACE2:3
for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.| by Lm3;

theorem :: CSSPACE2:4
for x, y being Complex holds 2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by Lm20;

theorem :: CSSPACE2:5
for x, y being Complex holds
( |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) & |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) ) by Lm21;

theorem :: CSSPACE2:6
canceled;

theorem :: CSSPACE2:7
for seq being Complex_Sequence holds Partial_Sums (seq *') = (Partial_Sums seq) *' by Lm1;

theorem :: CSSPACE2:8
for seq being Complex_Sequence
for n being Element of NAT st ( for i being Element of NAT holds
( (Re seq) . i >= 0 & (Im seq) . i = 0 ) ) holds
|.(Partial_Sums seq).| . n = (Partial_Sums |.seq.|) . n by Lm4;

theorem :: CSSPACE2:9
for seq being Complex_Sequence st seq is summable holds
Sum (seq *') = (Sum seq) *' by Lm5;

theorem :: CSSPACE2:10
for seq being Complex_Sequence st seq is absolutely_summable holds
|.(Sum seq).| <= Sum |.seq.| by Lm6;

theorem :: CSSPACE2:11
for seq being Complex_Sequence st seq is summable & ( for n being Element of NAT holds
( (Re seq) . n >= 0 & (Im seq) . n = 0 ) ) holds
|.(Sum seq).| = Sum |.seq.| by Lm7;

theorem :: CSSPACE2:12
for seq being Complex_Sequence
for n being Element of NAT holds
( (Re (seq (#) (seq *'))) . n >= 0 & (Im (seq (#) (seq *'))) . n = 0 ) by Lm8;

theorem :: CSSPACE2:13
for seq being Complex_Sequence st seq is absolutely_summable & Sum |.seq.| = 0 holds
for n being Element of NAT holds seq . n = 0c
proof
let seq be Complex_Sequence; ::_thesis: ( seq is absolutely_summable & Sum |.seq.| = 0 implies for n being Element of NAT holds seq . n = 0c )
assume that
A1: seq is absolutely_summable and
A2: Sum |.seq.| = 0 ; ::_thesis: for n being Element of NAT holds seq . n = 0c
A3: for n being Element of NAT holds (Partial_Sums |.seq.|) . n <= Sum |.seq.|
proof
let n be Element of NAT ; ::_thesis: (Partial_Sums |.seq.|) . n <= Sum |.seq.|
 (Partial_Sums |.seq.|) . n <= lim (Partial_Sums |.seq.|) by A1, SEQ_4:37;
hence  (Partial_Sums |.seq.|) . n <= Sum |.seq.| by SERIES_1:def_3; ::_thesis: verum
end;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_|.seq.|_._n_<>_0
assume  ex n being Element of NAT st |.seq.| . n <> 0 ; ::_thesis: contradiction
then consider n1 being Element of NAT  such that
A5: |.seq.| . n1 <> 0 ;
A6: for n being Element of NAT holds 0 <= (Partial_Sums |.seq.|) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums |.seq.|) . n
 |.seq.| . 0 = |.(seq . 0).| by VALUED_1:18;
then A7: 0 <= |.seq.| . 0 by COMPLEX1:46;
 ( n = n + 0 & (Partial_Sums |.seq.|) . 0 = |.seq.| . 0 ) by SERIES_1:def_1;
hence  0 <= (Partial_Sums |.seq.|) . n by A7, SEQM_3:5; ::_thesis: verum
end;
 (Partial_Sums |.seq.|) . n1 > 0
proof
now__::_thesis:_(_(_n1_=_0_&_(Partial_Sums_|.seq.|)_._n1_>_0_)_or_(_n1_<>_0_&_(Partial_Sums_|.seq.|)_._n1_>_0_)_)
percases ( n1 = 0 or n1 <> 0 ) ;
case n1 = 0 ; ::_thesis: (Partial_Sums |.seq.|) . n1 > 0
then  (Partial_Sums |.seq.|) . n1 <> 0 by A5, SERIES_1:def_1;
hence  (Partial_Sums |.seq.|) . n1 > 0 by A6; ::_thesis: verum
end;
caseA8: n1 <> 0 ; ::_thesis: (Partial_Sums |.seq.|) . n1 > 0
set nn = n1 - 1;
 |.seq.| . n1 = |.(seq . n1).| by VALUED_1:18;
then A9: ( (n1 - 1) + 1 = n1 & 0 <= |.seq.| . n1 ) by COMPLEX1:46;
 0 <= n1 by NAT_1:2;
then  0 + 1 <= n1 by A8, INT_1:7;
then A10: n1 - 1 is Element of NAT by INT_1:5;
then  0 <= (Partial_Sums |.seq.|) . (n1 - 1) by A6;
then  (|.seq.| . n1) + 0 <= (|.seq.| . n1) + ((Partial_Sums |.seq.|) . (n1 - 1)) by XREAL_1:7;
hence  (Partial_Sums |.seq.|) . n1 > 0 by A5, A10, A9, SERIES_1:def_1; ::_thesis: verum
end;
end;
end;
hence  (Partial_Sums |.seq.|) . n1 > 0 ; ::_thesis: verum
end;
hence  contradiction by A2, A3; ::_thesis: verum
end;
 for n being Element of NAT holds seq . n = 0c
proof
let n be Element of NAT ; ::_thesis: seq . n = 0c
0 = |.seq.| . n by A4
.= |.(seq . n).| by VALUED_1:18 ;
hence  seq . n = 0c by COMPLEX1:45; ::_thesis: verum
end;
hence  for n being Element of NAT holds seq . n = 0c ; ::_thesis: verum
end;

theorem :: CSSPACE2:14
for seq being Complex_Sequence holds |.seq.| = |.(seq *').| by Lm18;

theorem :: CSSPACE2:15
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm22;

theorem :: CSSPACE2:16
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm23;

theorem :: CSSPACE2:17
for c being Complex
for seq being Complex_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = |.((seq . m) - c).| * |.((seq . m) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| * |.((lim seq) - c).| ) by Lm22;

theorem :: CSSPACE2:18
for c being Complex
for seq1 being Real_Sequence
for seq being Complex_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = (|.((seq . i) - c).| * |.((seq . i) - c).|) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (|.((lim seq) - c).| * |.((lim seq) - c).|) + (lim seq1) ) by Lm23;