let u, v be VECTOR of Complex_l2_Space ; :: thesis: |.(seq_id u).| (#) |.(seq_id v).| is summable
A1: |.(seq_id v).| (#) |.(seq_id v).| is summable by CSSPACE:def 11, CSSPACE:def 20;
A2: |.(seq_id u).| (#) |.(seq_id u).| is summable by CSSPACE:def 11, CSSPACE:def 20;
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).|);
A3: (|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|) is summable by A1, A2, SERIES_1:10;
A4: for n being Element of NAT holds 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n
set rr = |.(seq_id u).| (#) |.(seq_id v).|;
A5: (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 ;
reconsider tt = abs ((|.(seq_id u).| (#) |.(seq_id v).|) . n) as Real ;
( 0 <= 2 & 0 <= tt ) by COMPLEX1:132;
hence 0 <= (2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|))) . n by A5, XREAL_1:129; :: thesis: verum

end;

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

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
set s = seq_id v;
set t = seq_id u;
reconsider sn = |.((seq_id v) . n).|, tn = |.((seq_id u) . n).| as Real ;
reconsider ss = abs sn, tt = abs tn as Real ;
A6: (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) ;
A7: ((|.(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 ;
0 <= ((abs sn) - (abs tn)) ^2 by XREAL_1:65;
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 A6, A7, 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;

then A8: 2 (#) (abs (|.(seq_id u).| (#) |.(seq_id v).|)) is summable by A3, A4, SERIES_1:24;
set q0 = 1 / 2;
(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 ;
then abs (|.(seq_id u).| (#) |.(seq_id v).|) is summable by A8, 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