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 = |.(|.(seq_id u).| (#) |.(seq_id v).|).|;
A1: for n being Nat holds 0 <= (2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n
proof
set rr = |.(seq_id u).| (#) |.(seq_id v).|;
let n be Nat; :: thesis: 0 <= (2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n
set tt = |.((|.(seq_id u).| (#) |.(seq_id v).|) . n).|;
A2: 0 <= |.((|.(seq_id u).| (#) |.(seq_id v).|) . n).| by COMPLEX1:46;
(2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n = 2 * (|.(|.(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 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n by A2; :: thesis: verum
end;
A3: for n being Nat holds (2 (#) |.(|.(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 Nat; :: thesis: (2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n <= ((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n
set sn = |.((seq_id v) . n).|;
set tn = |.((seq_id u) . n).|;
set ss = |.|.((seq_id v) . n).|.|;
set tt = |.|.((seq_id u) . n).|.|;
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
.= (|.((seq_id v) . n).| ^2) + ((|.(seq_id u).| . n) * (|.(seq_id u).| . n)) by VALUED_1:18
.= (|.((seq_id v) . n).| ^2) + (|.((seq_id u) . n).| * (|.(seq_id u).| . n)) by VALUED_1:18
.= (|.|.((seq_id v) . n).|.| ^2) + (|.|.((seq_id u) . n).|.| ^2) by VALUED_1:18 ;
A5: 0 <= (|.|.((seq_id v) . n).|.| - |.|.((seq_id u) . n).|.|) ^2 by XREAL_1:63;
(2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n = 2 * (|.(|.(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 * (|.(|.(seq_id u).| . n).| * |.(|.(seq_id v).| . n).|) by COMPLEX1:65
.= 2 * (|.|.((seq_id u) . n).|.| * |.(|.(seq_id v).| . n).|) by VALUED_1:18
.= 2 * (|.|.((seq_id v) . n).|.| * |.|.((seq_id u) . n).|.|) by VALUED_1:18
.= (2 * |.|.((seq_id v) . n).|.|) * |.|.((seq_id u) . n).|.| ;
then 0 + ((2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n) <= ((((|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|)) . n) - ((2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n)) + ((2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) . n) by A4, A5, XREAL_1:7;
hence (2 (#) |.(|.(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 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).|) = ((1 / 2) * 2) (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).| by SEQ_1:23
.= |.(|.(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;
then (|.(seq_id v).| (#) |.(seq_id v).|) + (|.(seq_id u).| (#) |.(seq_id u).|) is summable by SERIES_1:7;
then 2 (#) |.(|.(seq_id u).| (#) |.(seq_id v).|).| is summable by A1, A3, SERIES_1:20;
then |.(|.(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