:: RSSPACE2 semantic presentation

begin

theorem Th1: :: RSSPACE2:1
( the carrier of l2_Space = the_set_of_l2RealSequences & ( for x being set holds
( x is VECTOR of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) ) & 0. l2_Space = Zeroseq & ( for u being VECTOR of l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of l2_Space holds
( (seq_id v) (#) (seq_id w) is summable & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w)) ) ) ) )
proof
A1: for u, v being VECTOR of l2_Space holds (seq_id u) (#) (seq_id v) is summable
proof
set q0 = 1 / 2;
let u, v be VECTOR of 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));
A2: 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 ;
A3: 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 A3; ::_thesis: verum
end;
A4: 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 ;
A5: (((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
.= (sn ^2) + (((seq_id u) . n) * ((seq_id u) . n)) by SEQ_1:8
.= ((abs sn) ^2) + (tn ^2) by COMPLEX1:75
.= ((abs sn) ^2) + ((abs tn) ^2) by COMPLEX1:75 ;
A6: 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 * (ss * tt) by COMPLEX1:65
.= (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 A5, A6, 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;
A7: (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 RSSPACE:def_11, RSSPACE:def_13;
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 A2, A4, SERIES_1:20;
then  abs ((seq_id u) (#) (seq_id v)) is summable by A7, 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;
A8: for x being set holds
( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) )
proof
let x be set ; ::_thesis: ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) )
 ( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def_1;
hence  ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) by RSSPACE:def_11, RSSPACE:def_13; ::_thesis: verum
end;
A9: for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))
proof
let v, w be VECTOR of l2_Space; ::_thesis: v .|. w = Sum ((seq_id v) (#) (seq_id w))
thus v .|. w = the scalar of l2_Space . (v,w) by BHSP_1:def_1
.= Sum ((seq_id v) (#) (seq_id w)) by RSSPACE:def_12, RSSPACE:def_13 ; ::_thesis: verum
end;
A10: for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v)
proof
set W = the_set_of_l2RealSequences ;
set L1 = Linear_Space_of_RealSequences ;
let u, v be VECTOR of l2_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10, RSSPACE:12, RSSPACE:def_13;
 dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then  dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) = [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A11: [u,v] in dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) by RSSPACE:def_13, ZFMISC_1:87;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) . [u,v] by RSSPACE:def_8, RSSPACE:def_13
.= u1 + v1 by A11, FUNCT_1:47 ;
hence  u + v = (seq_id u) + (seq_id v) by RSSPACE:14; ::_thesis: verum
end;
A12: for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)
proof
set W = the_set_of_l2RealSequences ;
set L1 = Linear_Space_of_RealSequences ;
let r be Real; ::_thesis: for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of l2_Space; ::_thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10, RSSPACE:12, RSSPACE:def_13;
 dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then  dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) = [:REAL,the_set_of_l2RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A13: [r,u] in dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) by RSSPACE:def_13, ZFMISC_1:87;
r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) . [r,u] by RSSPACE:def_9, RSSPACE:def_13
.= r * u1 by A13, FUNCT_1:47 ;
hence  r * u = r (#) (seq_id u) by RSSPACE:14; ::_thesis: verum
end;
A14: for u being VECTOR of l2_Space holds u = seq_id u
proof
let u be VECTOR of l2_Space; ::_thesis: u = seq_id u
 u is VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10, RSSPACE:12, RSSPACE:def_13;
hence  u = seq_id u by RSSPACE:14; ::_thesis: verum
end;
A15: for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of l2_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by RLVECT_1:16
.= (- 1) (#) (seq_id u) by A12
.= - (seq_id u) by SEQ_1:17 ;
hence  ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A14; ::_thesis: verum
end;
A16: for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of l2_Space; ::_thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A10
.= (seq_id u) + (- (seq_id v)) by A15
.= (seq_id u) - (seq_id v) by SEQ_1:11 ; ::_thesis: verum
end;
0. l2_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def_10, RSSPACE:def_13
.= Zeroseq by RSSPACE:def_7 ;
hence  ( the carrier of l2_Space = the_set_of_l2RealSequences & ( for x being set holds
( x is VECTOR of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) ) & 0. l2_Space = Zeroseq & ( for u being VECTOR of l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of l2_Space holds
( (seq_id v) (#) (seq_id w) is summable & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w)) ) ) ) ) by A8, A14, A10, A12, A15, A16, A1, A9, RSSPACE:def_13; ::_thesis: verum
end;

theorem Th2: :: RSSPACE2:2
for x, y, z being Point of l2_Space
for a being Real holds
( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & 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 l2_Space; ::_thesis: for a being Real holds
( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let a be Real; ::_thesis: ( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
A1: for n being Element of NAT holds 0 <= ((seq_id x) (#) (seq_id x)) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= ((seq_id x) (#) (seq_id x)) . n
 ((seq_id x) (#) (seq_id x)) . n = ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8;
hence  0 <= ((seq_id x) (#) (seq_id x)) . n by XREAL_1:63; ::_thesis: verum
end;
A2: ( (seq_id x) (#) (seq_id x) is summable & x .|. x = Sum ((seq_id x) (#) (seq_id x)) ) by Th1;
A3: now__::_thesis:_(_x_.|._x_=_0_implies_x_=_0._l2_Space_)
A4: for n being Element of NAT holds 0 <= ((seq_id x) (#) (seq_id x)) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= ((seq_id x) (#) (seq_id x)) . n
 ((seq_id x) (#) (seq_id x)) . n = ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8;
hence  0 <= ((seq_id x) (#) (seq_id x)) . n by XREAL_1:63; ::_thesis: verum
end;
assume A5: x .|. x = 0 ; ::_thesis: x = 0. l2_Space
A6: ( x .|. x = Sum ((seq_id x) (#) (seq_id x)) & (seq_id x) (#) (seq_id x) is summable ) by Th1;
A7: for n being Element of NAT holds 0 = (seq_id x) . n
proof
let n be Element of NAT ; ::_thesis: 0 = (seq_id x) . n
0 = ((seq_id x) (#) (seq_id x)) . n by A5, A4, A6, RSSPACE:17
.= ((seq_id x) . n) * ((seq_id x) . n) by SEQ_1:8 ;
hence  0 = (seq_id x) . n by XCMPLX_1:6; ::_thesis: verum
end;
 x is Element of the_set_of_RealSequences by RSSPACE:def_11, RSSPACE:def_13;
hence  x = 0. l2_Space by A7, Th1, RSSPACE:def_6; ::_thesis: verum
end;
A8: x .|. y = Sum ((seq_id x) (#) (seq_id y)) by Th1
.= y .|. x by Th1 ;
A9: now__::_thesis:_(_x_=_0._l2_Space_implies_x_.|._x_=_0_)
assume A10: x = 0. l2_Space ; ::_thesis: x .|. x = 0
A11: 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 SEQ_1:8
.= ((seq_id x) . n) * 0 by A10, Th1, RSSPACE:def_6
.= 0 ; ::_thesis: verum
end;
thus x .|. x = Sum ((seq_id x) (#) (seq_id x)) by Th1
.= 0 by A11, RSSPACE:16 ; ::_thesis: verum
end;
A12: (seq_id x) (#) (seq_id y) is summable by Th1;
A13: (a * x) .|. y = Sum ((seq_id (a * x)) (#) (seq_id y)) by Th1
.= Sum ((seq_id (a (#) (seq_id x))) (#) (seq_id y)) by Th1
.= Sum ((a (#) (seq_id x)) (#) (seq_id y)) by RSSPACE:1
.= Sum (a (#) ((seq_id x) (#) (seq_id y))) by SEQ_1:18
.= a * (Sum ((seq_id x) (#) (seq_id y))) by A12, SERIES_1:10
.= a * (x .|. y) by Th1 ;
A14: ( (seq_id x) (#) (seq_id z) is summable & (seq_id y) (#) (seq_id z) is summable ) by Th1;
(x + y) .|. z = Sum ((seq_id (x + y)) (#) (seq_id z)) by Th1
.= Sum ((seq_id ((seq_id x) + (seq_id y))) (#) (seq_id z)) by Th1
.= Sum (((seq_id x) + (seq_id y)) (#) (seq_id z)) by RSSPACE:1
.= Sum (((seq_id x) (#) (seq_id z)) + ((seq_id y) (#) (seq_id z))) by SEQ_1:16
.= (Sum ((seq_id x) (#) (seq_id z))) + (Sum ((seq_id y) (#) (seq_id z))) by A14, SERIES_1:7
.= (x .|. z) + (Sum ((seq_id y) (#) (seq_id z))) by Th1
.= (x .|. z) + (y .|. z) by Th1 ;
hence  ( ( x .|. x = 0 implies x = 0. l2_Space ) & ( x = 0. l2_Space implies x .|. x = 0 ) & 0 <= x .|. x & x .|. y = y .|. x & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) ) by A3, A9, A1, A2, A8, A13, SERIES_1:18; ::_thesis: verum
end;

registration
cluster l2_Space  ->  RealUnitarySpace-like ;
coherence
 l2_Space is RealUnitarySpace-like by Th2, BHSP_1:def_2;
end;

Lm1:  for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) holds
( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) implies ( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) ) )
assume A1: for n being Element of NAT holds 0 <= rseq . n ; ::_thesis: ( ( for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )
A2: Partial_Sums rseq is V46() by A1, SERIES_1:16;
thus A3: for n being Element of NAT holds 0 <= (Partial_Sums rseq) . n ::_thesis: ( ( for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) ) )
proof
let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums rseq) . n
A4: ( n = n + 0 & (Partial_Sums rseq) . 0 = rseq . 0 ) by SERIES_1:def_1;
 0 <= rseq . 0 by A1;
hence  0 <= (Partial_Sums rseq) . n by A2, A4, SEQM_3:5; ::_thesis: verum
end;
thus A5: for n being Element of NAT holds rseq . n <= (Partial_Sums rseq) . n ::_thesis: ( rseq is summable implies ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) ) )
proof
let n be Element of NAT ; ::_thesis: rseq . n <= (Partial_Sums rseq) . n
now__::_thesis:_(_(_n_=_0_&_rseq_._n_<=_(Partial_Sums_rseq)_._n_)_or_(_n_<>_0_&_rseq_._n_<=_(Partial_Sums_rseq)_._n_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: rseq . n <= (Partial_Sums rseq) . n
hence  rseq . n <= (Partial_Sums rseq) . n by SERIES_1:def_1; ::_thesis: verum
end;
caseA6: n <> 0 ; ::_thesis: rseq . n <= (Partial_Sums rseq) . n
set nn = n - 1;
 0 + 1 <= n by A6, INT_1:7;
then A7: n - 1 in NAT by INT_1:5;
then  0 <= (Partial_Sums rseq) . (n - 1) by A3;
then  ( (n - 1) + 1 = n & (rseq . n) + 0 <= (rseq . n) + ((Partial_Sums rseq) . (n - 1)) ) by XREAL_1:7;
hence  rseq . n <= (Partial_Sums rseq) . n by A7, SERIES_1:def_1; ::_thesis: verum
end;
end;
end;
hence  rseq . n <= (Partial_Sums rseq) . n ; ::_thesis: verum
end;
assume  rseq is summable ; ::_thesis: ( ( for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Element of NAT holds rseq . n <= Sum rseq ) )
then A8: Partial_Sums rseq is bounded_above by A1, SERIES_1:17;
thus A9: for n being Element of NAT holds (Partial_Sums rseq) . n <= Sum rseq ::_thesis: for n being Element of NAT holds rseq . n <= Sum rseq
proof
let n be Element of NAT ; ::_thesis: (Partial_Sums rseq) . n <= Sum rseq
 (Partial_Sums rseq) . n <= lim (Partial_Sums rseq) by A1, A8, SEQ_4:37, SERIES_1:16;
hence  (Partial_Sums rseq) . n <= Sum rseq by SERIES_1:def_3; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: rseq . n <= Sum rseq
A10: rseq . n <= (Partial_Sums rseq) . n by A5;
 (Partial_Sums rseq) . n <= Sum rseq by A9;
hence  rseq . n <= Sum rseq by A10, XXREAL_0:2; ::_thesis: verum
end;

Lm2:  ( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) )
proof
A1: now__::_thesis:_for_x,_y_being_Real_holds_(x_+_y)_*_(x_+_y)_<=_((2_*_x)_*_x)_+_((2_*_y)_*_y)
let x, y be Real; ::_thesis: (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y)
 0 <= (x - y) ^2 by XREAL_1:63;
then  0 + ((x + y) * (x + y)) <= ((((2 * x) * x) + ((2 * y) * y)) - ((x + y) * (x + y))) + ((x + y) * (x + y)) by XREAL_1:7;
hence  (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Real_holds_x_*_x_<=_((2_*_(x_-_y))_*_(x_-_y))_+_((2_*_y)_*_y)
let x, y be Real; ::_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 Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) ) by A1; ::_thesis: verum
end;

Lm3:  for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof
let e be Real; ::_thesis: for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e ; ::_thesis: lim seq <= e
consider k being Element of NAT  such that
A3: for i being Element of NAT st k <= i holds
seq . i <= e by A2;
reconsider cseq = NAT --> e as Real_Sequence ;
A4: lim cseq = cseq . 0 by SEQ_4:26
.= e by FUNCOP_1:7 ;
A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_(seq_^\_k)_._i_<=_cseq_._i
let i be Element of NAT ; ::_thesis: (seq ^\ k) . i <= cseq . i
 ( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def_3;
hence  (seq ^\ k) . i <= cseq . i by FUNCOP_1:7; ::_thesis: verum
end;
 lim (seq ^\ k) = lim seq by A1, SEQ_4:20;
hence  lim seq <= e by A1, A5, A4, SEQ_2:18; ::_thesis: verum
end;

Lm4:  for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
proof
let c be Real; ::_thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
reconsider cseq = NAT --> c as Real_Sequence ;
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) )
assume A1: seq is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
A2: seq - cseq is convergent by A1, SEQ_2:11;
then A3: (seq - cseq) (#) (seq - cseq) is convergent by SEQ_2:14;
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) implies ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) )
assume A4: 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 A4
.= ((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 SEQ_1:10
.= ((seq . i) + ((- cseq) . i)) * ((seq . i) + ((- cseq) . i)) by SEQ_1:10
.= ((seq + (- cseq)) . i) * ((seq . i) + ((- cseq) . i)) by SEQ_1:7
.= ((seq + (- cseq)) . i) * ((seq + (- cseq)) . i) by SEQ_1:7
.= ((seq - cseq) . i) * ((seq + (- cseq)) . i) by SEQ_1:11
.= ((seq - cseq) . i) * ((seq - cseq) . i) by SEQ_1:11
.= ((seq - cseq) (#) (seq - cseq)) . i by SEQ_1:8 ; ::_thesis: verum
end;
then A5: for x being set st x in NAT holds
rseq . x = ((seq - cseq) (#) (seq - cseq)) . x ;
lim ((seq - cseq) (#) (seq - cseq)) = (lim (seq - cseq)) * (lim (seq - cseq)) by A2, SEQ_2:15
.= ((lim seq) - (lim cseq)) * (lim (seq - cseq)) by A1, SEQ_2:12
.= ((lim seq) - (lim cseq)) * ((lim seq) - (lim cseq)) by A1, SEQ_2:12
.= ((lim seq) - (cseq . 0)) * ((lim seq) - (lim cseq)) by SEQ_4:26
.= ((lim seq) - (cseq . 0)) * ((lim seq) - (cseq . 0)) by SEQ_4:26
.= ((lim seq) - c) * ((lim seq) - (cseq . 0)) by FUNCOP_1:7
.= ((lim seq) - c) * ((lim seq) - c) by FUNCOP_1:7 ;
hence  ( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) ) by A5, A3, FUNCT_2:12; ::_thesis: verum
end;

Lm5:  for c being Real
for seq, seq1 being Real_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 Real; ::_thesis: for seq, seq1 being Real_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, seq1 be Real_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 cseq = NAT --> c as Real_Sequence ;
A3: seq - cseq is convergent by A1, SEQ_2:11;
then A4: (seq - cseq) (#) (seq - cseq) is convergent by SEQ_2:14;
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 A5: 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 A5
.= (((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 SEQ_1:10
.= (((seq . i) + ((- cseq) . i)) * ((seq . i) + ((- cseq) . i))) + (seq1 . i) by SEQ_1:10
.= (((seq + (- cseq)) . i) * ((seq . i) + ((- cseq) . i))) + (seq1 . i) by SEQ_1:7
.= (((seq + (- cseq)) . i) * ((seq + (- cseq)) . i)) + (seq1 . i) by SEQ_1:7
.= (((seq - cseq) . i) * ((seq + (- cseq)) . i)) + (seq1 . i) by SEQ_1:11
.= (((seq - cseq) . i) * ((seq - cseq) . i)) + (seq1 . i) by SEQ_1:11
.= (((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 A6: rseq = ((seq - cseq) (#) (seq - cseq)) + seq1 by FUNCT_2:63;
lim ((seq - cseq) (#) (seq - cseq)) = (lim (seq - cseq)) * (lim (seq - cseq)) by A3, SEQ_2:15
.= ((lim seq) - (lim cseq)) * (lim (seq - cseq)) by A1, SEQ_2:12
.= ((lim seq) - (lim cseq)) * ((lim seq) - (lim cseq)) by A1, SEQ_2:12
.= ((lim seq) - (cseq . 0)) * ((lim seq) - (lim cseq)) by SEQ_4:26
.= ((lim seq) - (cseq . 0)) * ((lim seq) - (cseq . 0)) by SEQ_4:26
.= ((lim seq) - c) * ((lim seq) - (cseq . 0)) by FUNCOP_1:7
.= ((lim seq) - c) * ((lim seq) - c) by FUNCOP_1:7 ;
hence  ( rseq is convergent & lim rseq = (((lim seq) - c) * ((lim seq) - c)) + (lim seq1) ) by A2, A6, A4, SEQ_2:5, SEQ_2:6; ::_thesis: verum
end;

registration
cluster l2_Space  ->  complete ;
coherence
 l2_Space is complete
proof
let vseq be sequence of l2_Space; :: according to BHSP_3:def_4 ::_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 rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & c2 = lim rseqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in REAL & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( set ) ->  Element of REAL = (seq_id (vseq . c1)) . i;
consider rseqi being Real_Sequence such that
A3: for n being Element of NAT holds rseqi . n = H1(n) from SEQ_1:sch_1();
take  lim rseqi ; ::_thesis: ( lim rseqi in REAL & S1[x, lim rseqi] )
now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(rseqi_._k))_<_e
let e be real number ; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e )
assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ::_thesis: verum
proof
 e is Real by XREAL_0:def_1;
then 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, BHSP_3:2;
now__::_thesis:_for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((rseqi_._m)_-_(rseqi_._k))_<_e
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume  k <= m ; ::_thesis: abs ((rseqi . m) - (rseqi . k)) < e
then  ||.((vseq . m) - (vseq . k)).|| < e by A5;
then  sqrt (((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))) < e by BHSP_1:def_4;
then A6: sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) < e by Th1;
reconsider e1 = e as Real by XREAL_0:def_1;
A7: sqrt ((abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k)))) = sqrt ((abs ((rseqi . m) - (rseqi . k))) ^2)
.= abs ((rseqi . m) - (rseqi . k)) by COMPLEX1:46, SQUARE_1:22 ;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th1
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:1
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by SEQ_1:11 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then ((seq_id ((vseq . m) - (vseq . k))) . i) * ((seq_id ((vseq . m) - (vseq . k))) . i) = ((rseqi . m) - (rseqi . k)) ^2
.= (abs ((rseqi . m) - (rseqi . k))) ^2 by COMPLEX1:75
.= (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) ;
then A8: (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) = ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:8;
A9: 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;
hence  0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by XREAL_1:63; ::_thesis: verum
end;
A10: (seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))) is summable by RSSPACE:def_11, RSSPACE:def_13;
then A11: 0 <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) by A9, 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 A6, SQUARE_1:16;
then A12: Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) < e * e by A11, 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 A10, A9, Lm1;
then A13: ( 0 <= abs ((rseqi . m) - (rseqi . k)) & (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) < e * e ) by A12, A8, COMPLEX1:46, XXREAL_0:2;
sqrt (e * e) = sqrt (e1 ^2)
.= e by A4, SQUARE_1:22 ;
hence  abs ((rseqi . m) - (rseqi . k)) < e by A13, A7, SQUARE_1:27; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ; ::_thesis: verum
end;
end;
then  rseqi is convergent by SEQ_4:41;
hence  ( lim rseqi in REAL & S1[x, lim rseqi] ) by A3; ::_thesis: verum
end;
consider f being Function of NAT,REAL such that
A14: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider tseq = f as Real_Sequence ;
A15: now__::_thesis:_for_i_being_Element_of_NAT_ex_rseqi_being_Real_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_rseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_rseqi_is_convergent_&_tseq_._i_=_lim_rseqi_)
let i be Element of NAT ; ::_thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
 ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A14;
hence  ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; ::_thesis: verum
end;
A16: 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 A17: 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;
A18: e1 / 2 > 0 by A17, XREAL_1:215;
then consider k being Element of NAT  such that
A19: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, BHSP_3:2;
 e1 / 2 < e1 by A17, XREAL_1:216;
then A20: (e1 / 2) * (e1 / 2) < e1 * e1 by A18, XREAL_1:97;
A21: 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 A19;
then  sqrt (((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))) < e1 / 2 by BHSP_1:def_4;
then A22: sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))))) < e1 / 2 by Th1;
A23: 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))) . i) * ((seq_id ((vseq . n) - (vseq . m))) . i) by SEQ_1:8;
hence  0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i by XREAL_1:63; ::_thesis: verum
end;
 (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable by RSSPACE:def_11, RSSPACE:def_13;
then A24: 0 <= Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) by A23, SERIES_1:18;
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 A22, SQUARE_1:16;
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 A23, A24, RSSPACE:def_11, RSSPACE:def_13, SQUARE_1:def_2; ::_thesis: verum
end;
A25: 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[ 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 );
A26: 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 Th1
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE: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 A27: 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
A28: for m being Element of NAT holds rseqb . m = H1(m) from SEQ_1:sch_1();
consider rseq0 being Real_Sequence such that
A29: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A30: rseq0 is convergent and
A31: tseq . (i + 1) = lim rseq0 by A15;
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 A32: 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) )
A33: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_(((rseq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1)))_*_((rseq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1))))_+_(rseqb_._m)
let m be Element of NAT ; ::_thesis: rseq . m = (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . 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 A32
.= (((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 A26
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (rseqb . m) by A28
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + (rseqb . m) by A26
.= ((((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 SEQ_1:11
.= ((((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:11
.= ((((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 SEQ_1:7
.= ((((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 SEQ_1:7
.= ((((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 SEQ_1:10
.= ((((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 SEQ_1:10
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A29
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A29 ; ::_thesis: verum
end;
A34: rseqb is convergent by A27, A28;
then  lim rseq = (((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))) * ((tseq . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (lim rseqb) by A30, A31, A33, Lm5
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (lim rseqb) by SEQ_1:10
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:10
.= (((tseq + (- (seq_id (vseq . n)))) . (i + 1)) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:7
.= (((tseq + (- (seq_id (vseq . n)))) . (i + 1)) * ((tseq + (- (seq_id (vseq . n)))) . (i + 1))) + (lim rseqb) by SEQ_1:7
.= (((tseq - (seq_id (vseq . n))) . (i + 1)) * ((tseq + (- (seq_id (vseq . n)))) . (i + 1))) + (lim rseqb) by SEQ_1:11
.= (((tseq - (seq_id (vseq . n))) . (i + 1)) * ((tseq - (seq_id (vseq . n))) . (i + 1))) + (lim rseqb) by SEQ_1:11
.= (((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 A27, A28
.= (((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 RSSPACE: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 RSSPACE: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 A34, A30, A33, Lm5; ::_thesis: verum
end;
end;
then A35: 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 A36: 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 Real_Sequence such that
A37: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A38: rseq0 is convergent and
A39: tseq . 0 = lim rseq0 by A15;
A40: 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 A36
.= ((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 A26
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . 0 by A26
.= (((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 SEQ_1:11
.= (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0) by SEQ_1:11
.= (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0) by SEQ_1:7
.= (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)) * (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:7
.= (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))) * (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:10
.= (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)) * (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))) by SEQ_1:10
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) * (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)) by A37
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) * ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) by A37 ; ::_thesis: verum
end;
then  lim rseq = ((tseq . 0) + (- ((seq_id (vseq . n)) . 0))) * ((tseq . 0) - ((seq_id (vseq . n)) . 0)) by A38, A39, Lm4
.= ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) * ((tseq . 0) + (- ((seq_id (vseq . n)) . 0))) by SEQ_1:10
.= ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) * ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:10
.= ((tseq + (- (seq_id (vseq . n)))) . 0) * ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:7
.= ((tseq + (- (seq_id (vseq . n)))) . 0) * ((tseq + (- (seq_id (vseq . n)))) . 0) by SEQ_1:7
.= ((tseq - (seq_id (vseq . n))) . 0) * ((tseq + (- (seq_id (vseq . n)))) . 0) by SEQ_1:11
.= ((tseq - (seq_id (vseq . n))) . 0) * ((tseq - (seq_id (vseq . n))) . 0) by SEQ_1:11
.= ((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 RSSPACE:1
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 by RSSPACE: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 A38, A40, Lm4; ::_thesis: verum
end;
end;
then A41: S2[ 0 ] ;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A41, A35);
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 A42: 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 )
A43: 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
A44: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A45: 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 A46: 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 A21, A42, A46;
then A47: (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 Lm1;
A48: rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i by A44;
 Sum ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) < (e1 / 2) * (e1 / 2) by A21, A42, A46;
hence  rseq . m <= (e1 / 2) * (e1 / 2) by A48, A47, 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 A25, A44;
hence  (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2) by A45, Lm3; ::_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 A43;
hence  (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 * e1 by A20, XXREAL_0:2; ::_thesis: verum
end;
then A49: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above by SEQ_2:def_3;
A50: 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  ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable by A49, 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 A43, Lm3, SERIES_1:def_3;
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 A20, A50, A49, 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;
A51: (seq_id tseq) (#) (seq_id tseq) is summable
proof
set d = (seq_id tseq) (#) (seq_id tseq);
A52: 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
A53: 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 A16;
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 RSSPACE:def_11, RSSPACE:def_13;
then A54: 2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))) is summable by SERIES_1:10;
A55: 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
set x = (seq_id tseq) . i;
set y = (seq_id (vseq . m)) . i;
A56: 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) ;
((seq_id tseq) - (seq_id (vseq . m))) . i = ((seq_id tseq) + (- (seq_id (vseq . m)))) . i by SEQ_1:11
.= ((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i) by SEQ_1:7
.= ((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i)) by SEQ_1:10
.= ((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 A57: ( ((seq_id tseq) (#) (seq_id tseq)) . i = ((seq_id tseq) . i) * ((seq_id tseq) . i) & 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)) ) by SEQ_1:8;
((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 ;
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 A57, A56, Lm2; ::_thesis: verum
end;
 ((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))) is summable by A53;
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 A54, SERIES_1:7;
hence  (seq_id tseq) (#) (seq_id tseq) is summable by A52, A55, SERIES_1:20; ::_thesis: verum
end;
 tseq in the_set_of_RealSequences by RSSPACE:def_1;
then reconsider tv = tseq as Point of l2_Space by A51, RSSPACE:def_11, RSSPACE:def_13;
 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 A58: 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
A59: 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 A16, A58;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
 tseq in the_set_of_RealSequences by RSSPACE:def_1;
then reconsider u = tseq as VECTOR of l2_Space by A51, RSSPACE:def_11, RSSPACE:def_13;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume  n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then A60: Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e by A59;
reconsider v = vseq . n as VECTOR of l2_Space ;
 seq_id (u - v) = u - v by Th1;
then  seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Th1;
then A61: (u - v) .|. (u - v) < e * e by A60, Th1;
A62: ||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by BHSP_1:31
.= sqrt ((u - v) .|. (u - v)) by BHSP_1:def_4 ;
 0 <= (u - v) .|. (u - v) by BHSP_1:def_2;
then  sqrt ((u - v) .|. (u - v)) < sqrt (e ^2) by A61, SQUARE_1:27;
hence  ||.((vseq . n) - tv).|| < e by A58, A62, 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 BHSP_2:9; ::_thesis: verum
end;
end;

registration
clusterV78() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like complete for UNITSTR ;
existence
 ex b1 being RealUnitarySpace st b1 is complete
proof
take  l2_Space ; ::_thesis: l2_Space is complete
thus  l2_Space is complete ; ::_thesis: verum
end;
end;

definition
mode RealHilbertSpace is complete RealUnitarySpace;
end;

begin

theorem :: RSSPACE2:3
for r being Real_Sequence st ( for n being Element of NAT holds 0 <= r . n ) holds
( ( for n being Element of NAT holds 0 <= (Partial_Sums r) . n ) & ( for n being Element of NAT holds r . n <= (Partial_Sums r) . n ) & ( r is summable implies ( ( for n being Element of NAT holds (Partial_Sums r) . n <= Sum r ) & ( for n being Element of NAT holds r . n <= Sum r ) ) ) ) by Lm1;

theorem :: RSSPACE2:4
( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) ) by Lm2;

theorem :: RSSPACE2:5
for e being Real
for s being Real_Sequence st s is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
s . i <= e holds
lim s <= e by Lm3;

theorem :: RSSPACE2:6
for c being Real
for s being Real_Sequence st s is convergent holds
for r being Real_Sequence st ( for i being Element of NAT holds r . i = ((s . i) - c) * ((s . i) - c) ) holds
( r is convergent & lim r = ((lim s) - c) * ((lim s) - c) ) by Lm4;

theorem :: RSSPACE2:7
for c being Real
for s, s1 being Real_Sequence st s is convergent & s1 is convergent holds
for r being Real_Sequence st ( for i being Element of NAT holds r . i = (((s . i) - c) * ((s . i) - c)) + (s1 . i) ) holds
( r is convergent & lim r = (((lim s) - c) * ((lim s) - c)) + (lim s1) ) by Lm5;