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 S = seq1 (##) seq2;
set P1 = Partial_Sums seq1;
set P2 = Partial_Sums seq2;
set PA = Partial_Sums (abs seq1);
set P = Partial_Sums (seq1 (##) seq2);
set S1 = Sum seq1;
set S2 = Sum seq2;
A3: for e being real number st 0 < e holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e

proof

let e be real number ; :: thesis: ( 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e )
assume A4: 0 < e ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e
consider r being real number such that
A5: ( 0 < r & ( for k being Element of NAT holds abs (Sum (seq2 ^\ k)) < r ) ) by A2, Th56;

A6: now

let n be Element of NAT ; :: thesis: (abs seq1) . n >= 0
( abs (seq1 . n) = (abs seq1) . n & abs (seq1 . n) >= 0 ) by COMPLEX1:132, SEQ_1:16;
hence (abs seq1) . n >= 0 ; :: thesis: verum

end;

set e1 = e / (3 * ((abs (Sum seq2)) + 1));
set e2 = e / (3 * r);
set e3 = e / (3 * ((Sum (abs seq1)) + 1));
(abs (Sum seq2)) + 1 > 0 + 0 by COMPLEX1:132, XREAL_1:10;
then A7: 3 * ((abs (Sum seq2)) + 1) > 3 * 0 by XREAL_1:70;
then A8: e / (3 * ((abs (Sum seq2)) + 1)) > 0 by A4, XREAL_1:141;
seq1 is summable by A1, SERIES_1:40;
then ( Partial_Sums seq1 is convergent & lim (Partial_Sums seq1) = Sum seq1 & e / (3 * ((abs (Sum seq2)) + 1)) > 0 ) by A4, A7, SERIES_1:def 2, SERIES_1:def 3, XREAL_1:141;
then consider n0 being Element of NAT such that
A9: for n being Element of NAT st n0 <= n holds
abs (((Partial_Sums seq1) . n) - (Sum seq1)) < e / (3 * ((abs (Sum seq2)) + 1)) by SEQ_2:def 7;
A10: abs seq1 is summable by A1, SERIES_1:def 5;
3 * r > 0 * 3 by A5, XREAL_1:70;
then e / (3 * r) > 0 by A4, XREAL_1:141;
then consider n1 being Element of NAT such that
A11: for n being Element of NAT st n1 <= n holds
abs (((Partial_Sums (abs seq1)) . n) - ((Partial_Sums (abs seq1)) . n1)) < e / (3 * r) by A10, SERIES_1:25;
Sum (abs seq1) >= 0 by A6, A10, SERIES_1:21;
then (Sum (abs seq1)) + 1 > 0 + 0 ;
then 3 * ((Sum (abs seq1)) + 1) > 0 * 3 by XREAL_1:70;
then A12: ( e / (3 * ((Sum (abs seq1)) + 1)) > 0 & Partial_Sums seq2 is convergent & lim (Partial_Sums seq2) = Sum seq2 ) by A2, A4, SERIES_1:def 2, SERIES_1:def 3, XREAL_1:141;
then consider n2 being Element of NAT such that
A13: for n being Element of NAT st n2 <= n holds
abs (((Partial_Sums seq2) . n) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1)) by SEQ_2:def 7;
A14: ( max (n1 + 1),n2 = n1 + 1 or max (n1 + 1),n2 = n2 ) by XXREAL_0:16;
( max 1,n0 = 1 or max 1,n0 = n0 ) by XXREAL_0:16;
then reconsider M = max (max 1,n0),(max (n1 + 1),n2) as Element of NAT by A14, XXREAL_0:16;
take 2M = M * 2; :: thesis: for m being Element of NAT st 2M <= m holds
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e
let m be Element of NAT ; :: thesis: ( 2M <= m implies abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e )
assume A15: 2M <= m ; :: thesis: abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e
A16: ( 1 <= max 1,n0 & n0 <= max 1,n0 & max 1,n0 <= M & n1 + 1 <= max (n1 + 1),n2 & n2 <= max (n1 + 1),n2 & max (n1 + 1),n2 <= M & M <= M + M ) by NAT_1:11, XXREAL_0:25;
then A17: ( n0 <= M & n1 + 1 <= M & n2 <= M & 0 < M & M <= m ) by A15, XXREAL_0:2;
then reconsider M1 = M - 1 as Element of NAT by NAT_1:20;
( (abs (Sum seq2)) + 1 > 0 + 0 & (abs (Sum seq2)) + 1 > (abs (Sum seq2)) + 0 ) by COMPLEX1:132, XREAL_1:10;
then A18: ( (e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) = e / 3 & (e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) > (e / (3 * ((abs (Sum seq2)) + 1))) * (abs (Sum seq2)) ) by A8, XCMPLX_1:93, XREAL_1:70;
n0 <= m by A17, XXREAL_0:2;
then ( abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) = (abs (Sum seq2)) * (abs (((Partial_Sums seq1) . m) - (Sum seq1))) & abs (((Partial_Sums seq1) . m) - (Sum seq1)) < e / (3 * ((abs (Sum seq2)) + 1)) & abs (Sum seq2) >= 0 ) by A9, COMPLEX1:132, COMPLEX1:151;
then abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) <= (abs (Sum seq2)) * (e / (3 * ((abs (Sum seq2)) + 1))) by XREAL_1:66;
then A19: abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) < e / 3 by A18, XXREAL_0:2;
consider Fr being XFinSequence of such that
A20: (Partial_Sums (seq1 (##) seq2)) . m = ((Sum seq2) * ((Partial_Sums seq1) . m)) - (Sum Fr) and
A21: dom Fr = m + 1 and
A22: for i being Element of NAT st i in m + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((m -' i) + 1))) by A2, Th54;
consider absFr being XFinSequence of such that
A23: dom absFr = dom Fr and
A24: abs (Sum Fr) <= Sum absFr and
A25: for i being Element of NAT st i in dom absFr holds
absFr . i = abs (Fr . i) by Th55;
defpred S₁[ Element of NAT ] means ( $1 + 1 <= M implies Sum (absFr | ($1 + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . $1) );
A26: S₁[ 0 ]

proof

( Sum seq2 = ((Partial_Sums seq2) . (m -' 0 )) + (Sum (seq2 ^\ ((m -' 0 ) + 1))) & m -' 0 = m ) by A2, NAT_D:40, SERIES_1:18;
then A27: Sum (seq2 ^\ ((m -' 0 ) + 1)) = (Sum seq2) - ((Partial_Sums seq2) . m) ;
( 0 in m + 1 & dom (absFr | 0 ) = 0 ) by NAT_1:45;
then ( Sum (absFr | (0 + 1)) = (absFr . 0 ) + (Sum (absFr | 0 )) & Sum (absFr | 0 ) = 0 & absFr . 0 = abs (Fr . 0 ) & Fr . 0 = (seq1 . 0 ) * (Sum (seq2 ^\ ((m -' 0 ) + 1))) ) by A21, A22, A23, A25, Lm6, Lm8;
then A28: Sum (absFr | (0 + 1)) = (abs (seq1 . 0 )) * (abs (Sum (seq2 ^\ ((m -' 0 ) + 1)))) by COMPLEX1:151
.= ((abs seq1) . 0 ) * (abs (Sum (seq2 ^\ ((m -' 0 ) + 1)))) by SEQ_1:16
.= ((abs seq1) . 0 ) * (abs (((Partial_Sums seq2) . m) - (Sum seq2))) by A27, COMPLEX1:146 ;
( n2 <= M & M <= M + M ) by A16, XXREAL_0:2;
then n2 <= 2M by XXREAL_0:2;
then n2 <= m by A15, XXREAL_0:2;
then ( abs (((Partial_Sums seq2) . m) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1)) & (abs seq1) . 0 >= 0 ) by A6, A13;
then ((abs seq1) . 0 ) * (abs (((Partial_Sums seq2) . m) - (Sum seq2))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((abs seq1) . 0 ) by XREAL_1:66;
hence S₁[ 0 ] by A28, SERIES_1:def 1; :: thesis: verum

end;

A29: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A30: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
assume A31: (k + 1) + 1 <= M ; :: thesis: Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . (k + 1))
then A32: k + 1 < M by NAT_1:13;
then A33: ( k + 1 < m & m < m + 1 ) by A17, NAT_1:13, XXREAL_0:2;
then k + 1 < m + 1 by XXREAL_0:2;
then k + 1 in m + 1 by NAT_1:45;
then A34: ( Fr . (k + 1) = (seq1 . (k + 1)) * (Sum (seq2 ^\ ((m -' (k + 1)) + 1))) & abs (Fr . (k + 1)) = absFr . (k + 1) & Sum (absFr | ((k + 1) + 1)) = (absFr . (k + 1)) + (Sum (absFr | (k + 1))) ) by A21, A22, A23, A25, Lm8;
A35: Sum seq2 = ((Partial_Sums seq2) . (m -' (k + 1))) + (Sum (seq2 ^\ ((m -' (k + 1)) + 1))) by A2, SERIES_1:18;
( ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1)))) + (Sum (absFr | (k + 1))) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1)))) + ((e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . k)) & abs (seq1 . (k + 1)) = (abs seq1) . (k + 1) ) by A30, A31, NAT_1:13, SEQ_1:16, XREAL_1:8;
then ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1)))) + (Sum (absFr | (k + 1))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (((abs seq1) . (k + 1)) + ((Partial_Sums (abs seq1)) . k)) ;
then A36: ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1)))) + (Sum (absFr | (k + 1))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . (k + 1)) by SERIES_1:def 1;
( m - (k + 1) >= m - M & m - M >= 2M - M ) by A15, A32, XREAL_1:11, XREAL_1:12;
then m - (k + 1) >= M by XXREAL_0:2;
then ( m - (k + 1) >= n2 & m - (k + 1) = m -' (k + 1) ) by A17, A33, XREAL_1:235, XXREAL_0:2;
then abs (((Partial_Sums seq2) . (m -' (k + 1))) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1)) by A13;
then ( abs ((Sum seq2) - ((Partial_Sums seq2) . (m -' (k + 1)))) < e / (3 * ((Sum (abs seq1)) + 1)) & abs (seq1 . (k + 1)) >= 0 ) by COMPLEX1:132, COMPLEX1:146;
then (abs ((Sum seq2) - ((Partial_Sums seq2) . (m -' (k + 1))))) * (abs (seq1 . (k + 1))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1))) by XREAL_1:66;
then abs ((seq1 . (k + 1)) * (Sum (seq2 ^\ ((m -' (k + 1)) + 1)))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1))) by A35, COMPLEX1:151;
then Sum (absFr | ((k + 1) + 1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . (k + 1)))) + (Sum (absFr | (k + 1))) by A34, XREAL_1:8;
hence Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . (k + 1)) by A36, XXREAL_0:2; :: thesis: verum

end;

A37: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A26, A29);
(Partial_Sums (abs seq1)) . M1 <= Sum (abs seq1) by A6, A10, RSSPACE2:4;
then A38: (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum (abs seq1)) by A12, XREAL_1:66;
Sum (abs seq1) >= 0 by A6, A10, SERIES_1:21;
then ( (Sum (abs seq1)) + 1 > 0 + 0 & (Sum (abs seq1)) + 1 > (Sum (abs seq1)) + 0 ) by XREAL_1:10;
then ( ((Sum (abs seq1)) + 1) * (e / (3 * ((Sum (abs seq1)) + 1))) = e / 3 & (e / (3 * ((Sum (abs seq1)) + 1))) * ((Sum (abs seq1)) + 1) >= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum (abs seq1)) & M = M1 + 1 ) by A12, XCMPLX_1:93, XREAL_1:66;
then ( (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= e / 3 & Sum (absFr | M) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) ) by A37, A38, XXREAL_0:2;
then A39: Sum (absFr | M) <= e / 3 by XXREAL_0:2;
consider Fr1 being XFinSequence of such that
A40: absFr = (absFr | M) ^ Fr1 by Th5;
M < m + 1 by A17, NAT_1:13;
then M < len absFr by A21, A23;
then A41: ( m + 1 = (len (absFr | M)) + (len Fr1) & len (absFr | M) = M ) by A21, A23, A40, AFINSQ_1:14, AFINSQ_1:def 4;
defpred S₂[ Element of NAT ] means ( (M + $1) + 1 <= m + 1 implies Sum (Fr1 | ($1 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + $1)) - ((Partial_Sums (abs seq1)) . M1)) );
A42: S₂[ 0 ]

proof

assume A43: (M + 0 ) + 1 <= m + 1 ; :: thesis: Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0 )) - ((Partial_Sums (abs seq1)) . M1))
then ( (M + 1) - M <= (m + 1) - M & len Fr1 = (m + 1) - M ) by A41, XREAL_1:11;
then ( 1 c= len Fr1 & len Fr1 = dom Fr1 ) by NAT_1:40;
then ( dom (Fr1 | 1) = 1 & 0 in 1 ) by NAT_1:45, RELAT_1:91;
then A44: ( (Fr1 | 1) . 0 = Fr1 . 0 & Sum (Fr1 | 1) = (Fr1 | 1) . 0 ) by Lm7, FUNCT_1:70;
( M < m + 1 & m + 1 = len absFr ) by A21, A23, A43, NAT_1:13;
then ( absFr . M = Fr1 . (M - M) & M in m + 1 ) by A40, A41, AFINSQ_1:22, NAT_1:45;
then ( Fr1 . 0 = abs (Fr . M) & Fr . M = (seq1 . M) * (Sum (seq2 ^\ ((m -' M) + 1))) ) by A21, A22, A23, A25;
then A45: Fr1 . 0 = (abs (seq1 . M)) * (abs (Sum (seq2 ^\ ((m -' M) + 1)))) by COMPLEX1:151;
((Partial_Sums (abs seq1)) . M1) + ((abs seq1) . (M1 + 1)) = (Partial_Sums (abs seq1)) . (M1 + 1) by SERIES_1:def 1;
then ( ((Partial_Sums (abs seq1)) . M) - ((Partial_Sums (abs seq1)) . M1) = abs (seq1 . M) & abs (seq1 . M) >= 0 & r > abs (Sum (seq2 ^\ ((m -' M) + 1))) ) by A5, COMPLEX1:132, SEQ_1:16;
hence Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0 )) - ((Partial_Sums (abs seq1)) . M1)) by A44, A45, XREAL_1:66; :: thesis: verum

end;

A46: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A47: S₂[k] ; :: thesis: S₂[k + 1]
set k1 = k + 1;
set Mk1 = M + (k + 1);
assume A48: (M + (k + 1)) + 1 <= m + 1 ; :: thesis: Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + (k + 1))) - ((Partial_Sums (abs seq1)) . M1))
then ( M <= M + (k + 1) & M + (k + 1) < m + 1 & m + 1 = len absFr ) by A21, A23, NAT_1:11, NAT_1:13;
then ( absFr . (M + (k + 1)) = Fr1 . ((M + (k + 1)) - M) & M + (k + 1) in m + 1 ) by A40, A41, AFINSQ_1:22, NAT_1:45;
then A49: ( Fr1 . (k + 1) = abs (Fr . (M + (k + 1))) & Fr . (M + (k + 1)) = (seq1 . (M + (k + 1))) * (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))) ) by A21, A22, A23, A25;
then ( abs (Fr . (M + (k + 1))) = (abs (seq1 . (M + (k + 1)))) * (abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1)))) & abs (seq1 . (M + (k + 1))) >= 0 & abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))) < r ) by A5, COMPLEX1:132, COMPLEX1:151;
then A50: Fr1 . (k + 1) <= r * (abs (seq1 . (M + (k + 1)))) by A49, XREAL_1:66;
M + (k + 1) < m + 1 by A48, NAT_1:13;
then k + 1 < len Fr1 by A41, XREAL_1:9;
then ( k + 1 in len Fr1 & dom Fr1 = len Fr1 ) by NAT_1:45;
then ( Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1))) & Sum (Fr1 | (k + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + k)) - ((Partial_Sums (abs seq1)) . M1)) & abs (seq1 . (M + (k + 1))) = (abs seq1) . (M + (k + 1)) ) by A47, A48, Lm8, NAT_1:13, SEQ_1:16;
then Sum (Fr1 | ((k + 1) + 1)) <= (r * ((abs seq1) . (M + (k + 1)))) + (r * (((Partial_Sums (abs seq1)) . (M + k)) - ((Partial_Sums (abs seq1)) . M1))) by A50, XREAL_1:9;
then Sum (Fr1 | ((k + 1) + 1)) <= r * ((((abs seq1) . (M + (k + 1))) + ((Partial_Sums (abs seq1)) . (M + k))) - ((Partial_Sums (abs seq1)) . M1)) ;
then Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums (abs seq1)) . ((M + k) + 1)) - ((Partial_Sums (abs seq1)) . M1)) by SERIES_1:def 1;
hence Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + (k + 1))) - ((Partial_Sums (abs seq1)) . M1)) ; :: thesis: verum

end;

A51: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A42, A46);
M1 + 1 >= n1 + 1 by A16, XXREAL_0:2;
then M1 >= n1 by XREAL_1:10;
then ( (Partial_Sums (abs seq1)) . M1 >= (Partial_Sums (abs seq1)) . n1 & n1 + 1 <= m ) by A6, A17, Th57, XXREAL_0:2;
then ( ((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1) <= ((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1) & n1 <= m ) by NAT_1:13, XREAL_1:12;
then A52: ( r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) <= r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) & (Partial_Sums (abs seq1)) . m >= (Partial_Sums (abs seq1)) . n1 & abs (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) < e / (3 * r) ) by A5, A6, A11, Th57, XREAL_1:66;
then ((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1) >= ((Partial_Sums (abs seq1)) . n1) - ((Partial_Sums (abs seq1)) . n1) by XREAL_1:11;
then abs (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) = ((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1) by ABSVALUE:def 1;
then r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) <= r * (e / (3 * r)) by A5, A52, XREAL_1:66;
then A53: r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) <= r * (e / (3 * r)) by A52, XXREAL_0:2;
dom Fr1 = (m - M) + 1 by A41;
then ( Fr1 | ((m - M) + 1) = Fr1 & m = M + (m - M) & (M + (m - M)) + 1 <= m + 1 & m - M = m -' M ) by A17, RELAT_1:98, XREAL_1:235;
then Sum Fr1 <= r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) by A51;
then Sum Fr1 <= r * (e / (3 * r)) by A53, XXREAL_0:2;
then A54: Sum Fr1 <= e / 3 by A5, XCMPLX_1:93;
Sum absFr = addreal . (Sum (absFr | M)),(Sum Fr1) by A40, STIRL2_1:47;
then ( Sum absFr = (Sum (absFr | M)) + (Sum Fr1) & (Sum (absFr | M)) + (Sum Fr1) <= (e / 3) + (e / 3) ) by A39, A54, BINOP_2:def 9, XREAL_1:9;
then A55: abs (Sum Fr) <= (e / 3) + (e / 3) by A24, XXREAL_0:2;
((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2)) = ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) - (Sum Fr) by A20;
then ( abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) <= (abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1)))) + (abs (Sum Fr)) & (abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1)))) + (abs (Sum Fr)) < (e / 3) + ((e / 3) + (e / 3)) ) by A19, A55, COMPLEX1:143, XREAL_1:10;
hence abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e by XXREAL_0:2; :: thesis: verum

end;

then A56: 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, A56, SEQ_2:def 7;
hence Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) by SERIES_1:def 3; :: thesis: verum