let seq1, seq2 be Real_Sequence; :: thesis: ( seq1 is absolutely_summable & seq2 is summable implies ( seq1 (##) seq2 is summable & Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) ) )
assume that
A1: seq1 is absolutely_summable and
A2: seq2 is summable ; :: thesis: ( seq1 (##) seq2 is summable & Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) )
set S2 = Sum seq2;
set S1 = Sum seq1;
set PA = Partial_Sums |.seq1.|;
set P2 = Partial_Sums seq2;
set P1 = Partial_Sums seq1;
set S = seq1 (##) seq2;
set P = Partial_Sums (seq1 (##) seq2);
A3: for e being Real st 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e

proof

seq1 is summable by A1;
then A4: Partial_Sums seq1 is convergent by SERIES_1:def 2;
let e be Real; :: thesis: ( 0 < e implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e )
assume A5: 0 < e ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e
set e1 = e / (3 * (|.(Sum seq2).| + 1));
|.(Sum seq2).| + 1 > 0 + 0 by COMPLEX1:46, XREAL_1:8;
then A6: 3 * (|.(Sum seq2).| + 1) > 3 * 0 by XREAL_1:68;
then ( lim (Partial_Sums seq1) = Sum seq1 & e / (3 * (|.(Sum seq2).| + 1)) > 0 ) by A5, SERIES_1:def 3, XREAL_1:139;
then consider n0 being Nat such that
A7: for n being Nat st n0 <= n holds
|.(((Partial_Sums seq1) . n) - (Sum seq1)).| < e / (3 * (|.(Sum seq2).| + 1)) by A4, SEQ_2:def 7;
set e3 = e / (3 * ((Sum (abs seq1)) + 1));
|.(Sum seq2).| + 1 > 0 + 0 by COMPLEX1:46, XREAL_1:8;
then A8: (e / (3 * (|.(Sum seq2).| + 1))) * (|.(Sum seq2).| + 1) = e / 3 by XCMPLX_1:92;
A9: ( Partial_Sums seq2 is convergent & lim (Partial_Sums seq2) = Sum seq2 ) by A2, SERIES_1:def 2, SERIES_1:def 3;
consider r being Real such that
A10: 0 < r and
A11: for k being Nat holds |.(Sum (seq2 ^\ k)).| < r by A2, Th51;
set e2 = e / (3 * r);
A12: |.(Sum seq2).| + 1 > |.(Sum seq2).| + 0 by XREAL_1:8;

A13: now :: thesis: for n being Nat holds (abs seq1) . n >= 0

let n be Nat; :: thesis: (abs seq1) . n >= 0
|.(seq1 . n).| = (abs seq1) . n by SEQ_1:12;
hence (abs seq1) . n >= 0 by COMPLEX1:46; :: thesis: verum

end;

then A14: for n being Nat holds |.seq1.| . n >= 0 ;
A15: abs seq1 is summable by A1, SERIES_1:def 4;
then Sum (abs seq1) >= 0 by A14, SERIES_1:18;
then A16: ((Sum (abs seq1)) + 1) * (e / (3 * ((Sum (abs seq1)) + 1))) = e / 3 by XCMPLX_1:92;
A17: Sum (abs seq1) >= 0 by A15, A14, SERIES_1:18;
then 3 * ((Sum (abs seq1)) + 1) > 0 * 3 by XREAL_1:68;
then e / (3 * ((Sum (abs seq1)) + 1)) > 0 by A5, XREAL_1:139;
then consider n2 being Nat such that
A18: for n being Nat st n2 <= n holds
|.(((Partial_Sums seq2) . n) - (Sum seq2)).| < e / (3 * ((Sum (abs seq1)) + 1)) by A9, SEQ_2:def 7;
3 * r > 0 * 3 by A10, XREAL_1:68;
then e / (3 * r) > 0 by A5, XREAL_1:139;
then consider n1 being Nat such that
A19: for n being Nat st n1 <= n holds
|.(((Partial_Sums |.seq1.|) . n) - ((Partial_Sums |.seq1.|) . n1)).| < e / (3 * r) by A15, SERIES_1:21;
reconsider M = max ((max (1,n0)),(max ((n1 + 1),n2))) as Nat by TARSKI:1;
A20: max ((n1 + 1),n2) <= M by XXREAL_0:25;
take 2M = M * 2; :: thesis: for m being Nat st 2M <= m holds
|.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e
let m be Nat; :: thesis: ( 2M <= m implies |.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e )
assume A21: 2M <= m ; :: thesis: |.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e
A22: max (1,n0) <= M by XXREAL_0:25;
then 0 < M by XXREAL_0:25;
then reconsider M1 = M - 1 as Nat by NAT_1:20;
A23: M = M1 + 1 ;
A24: n1 + 1 <= max ((n1 + 1),n2) by XXREAL_0:25;
then M1 + 1 >= n1 + 1 by A20, XXREAL_0:2;
then M1 >= n1 by XREAL_1:8;
then (Partial_Sums |.seq1.|) . M1 >= (Partial_Sums |.seq1.|) . n1 by A13, Th52;
then ((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . M1) <= ((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1) by XREAL_1:10;
then A25: r * (((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . M1)) <= r * (((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1)) by A10, XREAL_1:64;
consider Fr being XFinSequence of REAL such that
A26: (Partial_Sums (seq1 (##) seq2)) . m = ((Sum seq2) * ((Partial_Sums seq1) . m)) - (Sum Fr) and
A27: dom Fr = m + 1 and
A28: for i being Nat st i in m + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((m -' i) + 1))) by A2, Th49;
consider absFr being XFinSequence of REAL such that
A29: dom absFr = dom Fr and
A30: |.(Sum Fr).| <= Sum absFr and
A31: for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| by Th50;
A32: M <= M + M by NAT_1:11;
then A33: M <= m by A21, XXREAL_0:2;
then M < len absFr by A27, A29, NAT_1:13;
then A34: len (absFr | M) = M by AFINSQ_1:11;
n1 + 1 <= M by A24, A20, XXREAL_0:2;
then n1 + 1 <= m by A33, XXREAL_0:2;
then A35: n1 <= m by NAT_1:13;
then (Partial_Sums |.seq1.|) . m >= (Partial_Sums |.seq1.|) . n1 by A13, Th52;
then ((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1) >= ((Partial_Sums |.seq1.|) . n1) - ((Partial_Sums |.seq1.|) . n1) by XREAL_1:9;
then A36: |.(((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1)).| = ((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1) by ABSVALUE:def 1;
consider Fr1 being XFinSequence of REAL such that
A37: absFr = (absFr | M) ^ Fr1 by Th1;
A38: m + 1 = (len (absFr | M)) + (len Fr1) by A27, A29, A37, AFINSQ_1:def 3;
then A39: Fr1 | ((m - M) + 1) = Fr1 by A34;
A40: n2 <= max ((n1 + 1),n2) by XXREAL_0:25;
then n2 <= M by A20, XXREAL_0:2;
then n2 <= 2M by A32, XXREAL_0:2;
then ( n2 <= m & m in NAT ) by A21, XXREAL_0:2, ORDINAL1:def 12;
then A41: |.(((Partial_Sums seq2) . m) - (Sum seq2)).| < e / (3 * ((Sum (abs seq1)) + 1)) by A18;
defpred S₁[ Nat] means ( (M + $1) + 1 <= m + 1 implies Sum (Fr1 | ($1 + 1)) <= r * (((Partial_Sums |.seq1.|) . (M + $1)) - ((Partial_Sums |.seq1.|) . M1)) );
A42: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A43: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
set Mk1 = M + (k + 1);
reconsider Mk = M + k as Nat ;
A44: |.(seq1 . (M + (k + 1))).| = (abs seq1) . (M + (k + 1)) by SEQ_1:12;
assume A45: (M + (k + 1)) + 1 <= m + 1 ; :: thesis: Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums |.seq1.|) . (M + (k + 1))) - ((Partial_Sums |.seq1.|) . M1))
then A46: M + (k + 1) < m + 1 by NAT_1:13;
then A47: M + (k + 1) in Segm (m + 1) by NAT_1:44;
then Fr . (M + (k + 1)) = (seq1 . (M + (k + 1))) * (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))) by A28;
then A48: |.(Fr . (M + (k + 1))).| = |.(seq1 . (M + (k + 1))).| * |.(Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))).| by COMPLEX1:65;
M + (k + 1) < m + 1 by A45, NAT_1:13;
then k + 1 < len Fr1 by A38, A34, XREAL_1:7;
then k + 1 in len Fr1 by AFINSQ_1:86;
then A49: Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1))) by AFINSQ_2:65;
m + 1 = len absFr by A27, A29;
then absFr . (M + (k + 1)) = Fr1 . ((M + (k + 1)) - M) by A37, A34, A46, AFINSQ_1:19, NAT_1:11;
then A50: Fr1 . (k + 1) = |.(Fr . (M + (k + 1))).| by A27, A29, A31, A47;
A51: (|.seq1.| . (Mk + 1)) + ((Partial_Sums |.seq1.|) . Mk) = (Partial_Sums |.seq1.|) . (Mk + 1) by SERIES_1:def 1;
( |.(seq1 . (M + (k + 1))).| >= 0 & |.(Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))).| < r ) by A11, COMPLEX1:46;
then Fr1 . (k + 1) <= r * |.(seq1 . (M + (k + 1))).| by A50, A48, XREAL_1:64;
then Sum (Fr1 | ((k + 1) + 1)) <= (r * (|.seq1.| . (M + (k + 1)))) + (r * (((Partial_Sums |.seq1.|) . (M + k)) - ((Partial_Sums |.seq1.|) . M1))) by A43, A45, A49, A44, NAT_1:13, XREAL_1:7;
then Sum (Fr1 | ((k + 1) + 1)) <= r * (((|.seq1.| . (M + (k + 1))) + ((Partial_Sums |.seq1.|) . (M + k))) - ((Partial_Sums |.seq1.|) . M1)) ;
then Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums |.seq1.|) . ((M + k) + 1)) - ((Partial_Sums |.seq1.|) . M1)) by A51;
hence Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums |.seq1.|) . (M + (k + 1))) - ((Partial_Sums |.seq1.|) . M1)) ; :: thesis: verum

end;

|.(((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1)).| < e / (3 * r) by A19, A35;
then r * (((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . n1)) <= r * (e / (3 * r)) by A10, A36, XREAL_1:64;
then A52: r * (((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . M1)) <= r * (e / (3 * r)) by A25, XXREAL_0:2;
A53: ( m = M + (m - M) & m - M = m -' M ) by A21, A32, XREAL_1:233, XXREAL_0:2;
A54: S₁[ 0 ]

proof

assume A55: (M + 0) + 1 <= m + 1 ; :: thesis: Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums |.seq1.|) . (M + 0)) - ((Partial_Sums |.seq1.|) . M1))
then A56: M < m + 1 by NAT_1:13;
then A57: M in Segm (m + 1) by NAT_1:44;
then A58: Fr . M = (seq1 . M) * (Sum (seq2 ^\ ((m -' M) + 1))) by A28;
(M + 1) - M <= (m + 1) - M by A55, XREAL_1:9;
then Segm 1 c= Segm (len Fr1) by A38, A34, NAT_1:39;
then A59: dom (Fr1 | 1) = 1 by RELAT_1:62;
m + 1 = len absFr by A27, A29;
then absFr . M = Fr1 . (M - M) by A37, A34, A56, AFINSQ_1:19;
then Fr1 . 0 = |.(Fr . M).| by A27, A29, A31, A57;
then A60: Fr1 . 0 = |.(seq1 . M).| * |.(Sum (seq2 ^\ ((m -' M) + 1))).| by A58, COMPLEX1:65;
A61: ( |.(seq1 . M).| >= 0 & r > |.(Sum (seq2 ^\ ((m -' M) + 1))).| ) by A11, COMPLEX1:46;
0 in Segm 1 by NAT_1:44;
then A62: (Fr1 | 1) . 0 = Fr1 . 0 by A59, FUNCT_1:47;
((Partial_Sums |.seq1.|) . M1) + (|.seq1.| . (M1 + 1)) = (Partial_Sums |.seq1.|) . (M1 + 1) by SERIES_1:def 1;
then A63: ((Partial_Sums |.seq1.|) . M) - ((Partial_Sums |.seq1.|) . M1) = |.(seq1 . M).| by SEQ_1:12;
Sum (Fr1 | 1) = (Fr1 | 1) . 0 by A59, Lm3;
hence Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums |.seq1.|) . (M + 0)) - ((Partial_Sums |.seq1.|) . M1)) by A62, A60, A63, A61, XREAL_1:64; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A54, A42);
then Sum Fr1 <= r * (((Partial_Sums |.seq1.|) . m) - ((Partial_Sums |.seq1.|) . M1)) by A39, A53;
then Sum Fr1 <= r * (e / (3 * r)) by A52, XXREAL_0:2;
then A64: Sum Fr1 <= e / 3 by A10, XCMPLX_1:92;
|.seq1.| . 0 >= 0 by A13;
then A65: (|.seq1.| . 0) * |.(((Partial_Sums seq2) . m) - (Sum seq2)).| <= (e / (3 * ((Sum (abs seq1)) + 1))) * (|.seq1.| . 0) by A41, XREAL_1:64;
A66: 0 in Segm (m + 1) by NAT_1:44;
then A67: Fr . 0 = (seq1 . 0) * (Sum (seq2 ^\ ((m -' 0) + 1))) by A28;
(Partial_Sums |.seq1.|) . M1 <= Sum |.seq1.| by A14, A15, RSSPACE2:3;
then A68: (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . M1) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum |.seq1.|) by A5, A17, XREAL_1:64;
( Sum seq2 = ((Partial_Sums seq2) . (m -' 0)) + (Sum (seq2 ^\ ((m -' 0) + 1))) & m -' 0 = m ) by A2, NAT_D:40, SERIES_1:15;
then A69: Sum (seq2 ^\ ((m -' 0) + 1)) = (Sum seq2) - ((Partial_Sums seq2) . m) ;
n0 <= max (1,n0) by XXREAL_0:25;
then n0 <= M by A22, XXREAL_0:2;
then ( n0 <= m & m in NAT ) by A33, XXREAL_0:2, ORDINAL1:def 12;
then A70: |.(((Partial_Sums seq1) . m) - (Sum seq1)).| < e / (3 * (|.(Sum seq2).| + 1)) by A7;
( |.((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))).| = |.(Sum seq2).| * |.(((Partial_Sums seq1) . m) - (Sum seq1)).| & |.(Sum seq2).| >= 0 ) by COMPLEX1:46, COMPLEX1:65;
then A71: |.((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))).| <= |.(Sum seq2).| * (e / (3 * (|.(Sum seq2).| + 1))) by A70, XREAL_1:64;
A72: Sum absFr = (Sum (absFr | M)) + (Sum Fr1) by A37, AFINSQ_2:55;
defpred S₂[ Nat] means ( $1 + 1 <= M implies Sum (absFr | ($1 + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . $1) );
A73: n2 <= M by A40, A20, XXREAL_0:2;
A74: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A75: S₂[k] ; :: thesis: S₂[k + 1]
reconsider k1 = k + 1 as Nat ;
A76: |.(seq1 . k1).| = (abs seq1) . k1 by SEQ_1:12;
A77: m - M >= 2M - M by A21, XREAL_1:9;
assume A78: (k + 1) + 1 <= M ; :: thesis: Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . (k + 1))
then A79: k1 < M by NAT_1:13;
then m - k1 >= m - M by XREAL_1:10;
then m - k1 >= M by A77, XXREAL_0:2;
then A80: m - k1 >= n2 by A73, XXREAL_0:2;
((e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).|) + (Sum (absFr | k1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).|) + ((e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . k)) by A75, A78, NAT_1:13, XREAL_1:6;
then ( ((e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).|) + (Sum (absFr | k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (((abs seq1) . k1) + ((Partial_Sums |.seq1.|) . k)) & k in NAT ) by A76, ORDINAL1:def 12;
then A81: ((e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).|) + (Sum (absFr | k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . k1) by SERIES_1:def 1;
k1 < m by A33, A79, XXREAL_0:2;
then k1 < m + 1 by NAT_1:13;
then A82: k1 in Segm (m + 1) by NAT_1:44;
then A83: Sum (absFr | (k1 + 1)) = (absFr . k1) + (Sum (absFr | k1)) by A27, A29, AFINSQ_2:65;
m - k1 = m -' k1 by A33, A79, XREAL_1:233, XXREAL_0:2;
then |.(((Partial_Sums seq2) . (m -' k1)) - (Sum seq2)).| < e / (3 * ((Sum (abs seq1)) + 1)) by A18, A80;
then A84: |.((Sum seq2) - ((Partial_Sums seq2) . (m -' k1))).| < e / (3 * ((Sum (abs seq1)) + 1)) by COMPLEX1:60;
A85: Sum seq2 = ((Partial_Sums seq2) . (m -' k1)) + (Sum (seq2 ^\ ((m -' k1) + 1))) by A2, SERIES_1:15;
|.(seq1 . k1).| >= 0 by COMPLEX1:46;
then |.((Sum seq2) - ((Partial_Sums seq2) . (m -' k1))).| * |.(seq1 . k1).| <= (e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).| by A84, XREAL_1:64;
then A86: |.((seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1)))).| <= (e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).| by A85, COMPLEX1:65;
( Fr . k1 = (seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1))) & |.(Fr . k1).| = absFr . k1 ) by A27, A28, A29, A31, A82;
then Sum (absFr | (k1 + 1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * |.(seq1 . k1).|) + (Sum (absFr | k1)) by A83, A86, XREAL_1:6;
hence Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . (k + 1)) by A81, XXREAL_0:2; :: thesis: verum

end;

A87: Sum (absFr | zz) = 0 ;
( Sum (absFr | (zz + 1)) = (absFr . 0) + (Sum (absFr | zz)) & absFr . 0 = |.(Fr . 0).| ) by A27, A29, A31, A66, AFINSQ_2:65;
then Sum (absFr | (zz + 1)) = |.(seq1 . 0).| * |.(Sum (seq2 ^\ ((m -' 0) + 1))).| by A67, A87, COMPLEX1:65
.= ((abs seq1) . 0) * |.(Sum (seq2 ^\ ((m -' 0) + 1))).| by SEQ_1:12
.= ((abs seq1) . 0) * |.(((Partial_Sums seq2) . m) - (Sum seq2)).| by A69, COMPLEX1:60 ;
then A88: S₂[ 0 ] by A65, SERIES_1:def 1;
for k being Nat holds S₂[k] from NAT_1:sch 2(A88, A74);
then A89: Sum (absFr | M) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . M1) by A23;
(Sum (abs seq1)) + 1 > (Sum (abs seq1)) + 0 by XREAL_1:8;
then (e / (3 * ((Sum (abs seq1)) + 1))) * ((Sum (abs seq1)) + 1) >= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum (abs seq1)) by A5, A17, XREAL_1:64;
then (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums |.seq1.|) . M1) <= e / 3 by A68, A16, XXREAL_0:2;
then Sum (absFr | M) <= e / 3 by A89, XXREAL_0:2;
then (Sum (absFr | M)) + (Sum Fr1) <= (e / 3) + (e / 3) by A64, XREAL_1:7;
then A90: |.(Sum Fr).| <= (e / 3) + (e / 3) by A30, A72, XXREAL_0:2;
((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2)) = ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) - (Sum Fr) by A26;
then A91: |.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| <= |.((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))).| + |.(Sum Fr).| by COMPLEX1:57;
e / (3 * (|.(Sum seq2).| + 1)) > 0 by A5, A6, XREAL_1:139;
then (e / (3 * (|.(Sum seq2).| + 1))) * (|.(Sum seq2).| + 1) > (e / (3 * (|.(Sum seq2).| + 1))) * |.(Sum seq2).| by A12, XREAL_1:68;
then |.((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))).| < e / 3 by A8, A71, XXREAL_0:2;
then |.((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))).| + |.(Sum Fr).| < (e / 3) + ((e / 3) + (e / 3)) by A90, XREAL_1:8;
hence |.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e by A91, XXREAL_0:2; :: thesis: verum

end;

then A92: Partial_Sums (seq1 (##) seq2) is convergent by SEQ_2:def 6;
hence seq1 (##) seq2 is summable by SERIES_1:def 2; :: thesis: Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2)
lim (Partial_Sums (seq1 (##) seq2)) = (Sum seq1) * (Sum seq2) by A3, A92, SEQ_2:def 7;
hence Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) by SERIES_1:def 3; :: thesis: verum