thus
the carrier of l2_Space = the_set_of_l2RealSequences
; :: thesis: ( ( 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)) ) )

thus for x being set holds

( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) :: thesis: ( 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)) ) )

.= Zeroseq ; :: thesis: ( ( 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)) ) )

thus for u being VECTOR of l2_Space holds u = seq_id u ; :: thesis: ( ( 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)) ) )

set W = the_set_of_l2RealSequences ;

set L1 = Linear_Space_of_RealSequences ;

thus A10: for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) :: thesis: ( ( 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)) ) )

for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) :: thesis: ( ( 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)) ) )

( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) :: thesis: ( ( 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)) ) )

( 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)) ) )

thus for x being set holds

( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) :: thesis: ( 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

thus 0. l2_Space =
0. Linear_Space_of_RealSequences
by RSSPACE:def 10
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 FUNCT_2:8, FUNCT_2:66;

hence ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) by RSSPACE:def 11; :: thesis: verum

end;( x in the_set_of_RealSequences iff x is Real_Sequence ) by FUNCT_2:8, FUNCT_2:66;

hence ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) by RSSPACE:def 11; :: thesis: verum

.= Zeroseq ; :: thesis: ( ( 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)) ) )

thus for u being VECTOR of l2_Space holds u = seq_id u ; :: thesis: ( ( 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)) ) )

set W = the_set_of_l2RealSequences ;

set L1 = Linear_Space_of_RealSequences ;

thus A10: for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) :: thesis: ( ( 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

thus A12:
for r being Real
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;

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 ZFMISC_1:87;

u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) . [u,v] by RSSPACE:def 8

.= u1 + v1 by A11, FUNCT_1:47 ;

hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2; :: thesis: verum

end;reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:10, RSSPACE:12;

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 ZFMISC_1:87;

u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) . [u,v] by RSSPACE:def 8

.= u1 + v1 by A11, FUNCT_1:47 ;

hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2; :: thesis: verum

for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) :: thesis: ( ( 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

thus A15:
for u being VECTOR of l2_Space holds
let r be Real; :: thesis: for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)

reconsider r = r as Element of REAL by XREAL_0:def 1;

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;

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 ZFMISC_1:87;

r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) . [r,u] by RSSPACE:def 9

.= r * u1 by A13, FUNCT_1:47 ;

hence r * u = r (#) (seq_id u) by RSSPACE:3; :: thesis: verum

end;reconsider r = r as Element of REAL by XREAL_0:def 1;

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;

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 ZFMISC_1:87;

r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) . [r,u] by RSSPACE:def 9

.= r * u1 by A13, FUNCT_1:47 ;

hence r * u = r (#) (seq_id u) by RSSPACE:3; :: thesis: verum

( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) :: thesis: ( ( 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

thus
for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v)
:: thesis: ( ( 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)) ) )
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) ) ; :: thesis: verum

end;- 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) ) ; :: thesis: verum

proof

thus
for u, v being VECTOR of l2_Space holds (seq_id u) (#) (seq_id v) is summable
:: thesis: for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))
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;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

proof

thus
for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))
:: thesis: verum
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 Nat holds 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

.= 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;

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;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 Nat holds 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

proof

A4:
for n being Nat holds (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n <= (((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u))) . n
set rr = (seq_id u) (#) (seq_id v);

let n be Nat; :: thesis: 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

reconsider tt = |.(((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 * |.(((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;let n be Nat; :: thesis: 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

reconsider tt = |.(((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 * |.(((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

proof

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
set s = seq_id v;

set t = seq_id u;

let n be 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 = |.sn.|, tt = |.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

.= (|.sn.| ^2) + (tn ^2) by COMPLEX1:75

.= (|.sn.| ^2) + (|.tn.| ^2) by COMPLEX1:75 ;

A6: 0 <= (|.sn.| - |.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 * |.(((seq_id u) (#) (seq_id v)) . n).| by SEQ_1:12

.= 2 * |.(((seq_id u) . n) * ((seq_id v) . n)).| by SEQ_1:8

.= 2 * (ss * tt) by COMPLEX1:65

.= (2 * |.sn.|) * |.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;set t = seq_id u;

let n be 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 = |.sn.|, tt = |.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

.= (|.sn.| ^2) + (tn ^2) by COMPLEX1:75

.= (|.sn.| ^2) + (|.tn.| ^2) by COMPLEX1:75 ;

A6: 0 <= (|.sn.| - |.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 * |.(((seq_id u) (#) (seq_id v)) . n).| by SEQ_1:12

.= 2 * |.(((seq_id u) . n) * ((seq_id v) . n)).| by SEQ_1:8

.= 2 * (ss * tt) by COMPLEX1:65

.= (2 * |.sn.|) * |.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

.= 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;

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