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:132;
(2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n = 2 * ((abs (|.(seq_id u).| (#) |.(seq_id v).|)) . n) by SEQ_1:13
.= 2 * (abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n)) by SEQ_1:16 ;
hence 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n by A2, XREAL_1:129; :: 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:11
.= ((|.(seq_id v).| . n) * (|.(seq_id v).| . n)) + ((|.(seq_id u).| (#) |.(seq_id u).|) . n) by SEQ_1:12
.= ((|.(seq_id v).| . n) * (|.(seq_id v).| . n)) + ((|.(seq_id u).| . n) * (|.(seq_id u).| . n)) by SEQ_1:12
.= (|.((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:65;
(2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n = 2 * ((abs (|.(seq_id u).| (#) |.(seq_id v).|)) . n) by SEQ_1:13
.= 2 * (abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n)) by SEQ_1:16
.= 2 * (abs ((|.(seq_id u).| . n) * (|.(seq_id v).| . n))) by SEQ_1:12
.= 2 * ((abs (|.(seq_id u).| . n)) * (abs (|.(seq_id v).| . n))) by COMPLEX1:151
.= 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:9;
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:31
.= abs (|.(seq_id u).| (#) |.(seq_id v).|) by SEQ_1:35 ;
( |.(seq_id v).| (#) |.(seq_id v).| is summable & |.(seq_id u).| (#) |.(seq_id u).| is summable ) by CSSPACE:def 11, CSSPACE:def 20;
then (|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|) is summable by SERIES_1:10;
then 2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|)) is summable by A1, A3, SERIES_1:24;
then abs (|.(seq_id u).| (#) |.(seq_id v).|) is summable by A6, SERIES_1:13;
then |.(seq_id u).| (#) |.(seq_id v).| is absolutely_summable by SERIES_1:def 5;
hence |.(seq_id u).| (#) |.(seq_id v).| is summable ; :: thesis: verum