let seq1, seq2 be Real_Sequence; ( 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
; ( seq1 (##) seq2 is summable & Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) )
set S2 = Sum seq2;
set S1 = Sum seq1;
set PA = Partial_Sums (abs 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 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
seq1 is
summable
by A1, SERIES_1:35;
then A4:
Partial_Sums seq1 is
convergent
by SERIES_1:def 2;
let e be
real number ;
( 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 A5:
0 < e
;
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
set e1 =
e / (3 * ((abs (Sum seq2)) + 1));
(abs (Sum seq2)) + 1
> 0 + 0
by COMPLEX1:46, XREAL_1:8;
then A6:
3
* ((abs (Sum seq2)) + 1) > 3
* 0
by XREAL_1:68;
then
(
lim (Partial_Sums seq1) = Sum seq1 &
e / (3 * ((abs (Sum seq2)) + 1)) > 0 )
by A5, SERIES_1:def 3, XREAL_1:139;
then consider n0 being
Element of
NAT such that A7:
for
n being
Element of
NAT st
n0 <= n holds
abs (((Partial_Sums seq1) . n) - (Sum seq1)) < e / (3 * ((abs (Sum seq2)) + 1))
by A4, SEQ_2:def 7;
set e3 =
e / (3 * ((Sum (abs seq1)) + 1));
A8:
(
max (1,
n0)
= 1 or
max (1,
n0)
= n0 )
by XXREAL_0:16;
(abs (Sum seq2)) + 1
> 0 + 0
by COMPLEX1:46, XREAL_1:8;
then A9:
(e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) = e / 3
by XCMPLX_1:92;
A10:
(
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 number such that A11:
0 < r
and A12:
for
k being
Nat holds
abs (Sum (seq2 ^\ k)) < r
by A2, Th56;
set e2 =
e / (3 * r);
A13:
(abs (Sum seq2)) + 1
> (abs (Sum seq2)) + 0
by XREAL_1:8;
then A15:
for
n being
Element of
NAT holds
(abs seq1) . n >= 0
;
A16:
abs seq1 is
summable
by A1, SERIES_1:def 4;
then
Sum (abs seq1) >= 0
by A15, SERIES_1:18;
then A17:
((Sum (abs seq1)) + 1) * (e / (3 * ((Sum (abs seq1)) + 1))) = e / 3
by XCMPLX_1:92;
A18:
Sum (abs seq1) >= 0
by A16, A15, 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
Element of
NAT such that A19:
for
n being
Element of
NAT st
n2 <= n holds
abs (((Partial_Sums seq2) . n) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1))
by A10, SEQ_2:def 7;
3
* r > 0 * 3
by A11, XREAL_1:68;
then
e / (3 * r) > 0
by A5, XREAL_1:139;
then consider n1 being
Element of
NAT such that A20:
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 A16, SERIES_1:21;
(
max (
(n1 + 1),
n2)
= n1 + 1 or
max (
(n1 + 1),
n2)
= n2 )
by XXREAL_0:16;
then reconsider M =
max (
(max (1,n0)),
(max ((n1 + 1),n2))) as
Element of
NAT by A8, XXREAL_0:16;
A21:
max (
(n1 + 1),
n2)
<= M
by XXREAL_0:25;
take 2M =
M * 2;
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 ;
( 2M <= m implies abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e )
assume A22:
2M <= m
;
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e
A23:
max (1,
n0)
<= M
by XXREAL_0:25;
then
0 < M
by XXREAL_0:25;
then reconsider M1 =
M - 1 as
Element of
NAT by NAT_1:20;
A24:
M = M1 + 1
;
A25:
n1 + 1
<= max (
(n1 + 1),
n2)
by XXREAL_0:25;
then
M1 + 1
>= n1 + 1
by A21, XXREAL_0:2;
then
M1 >= n1
by XREAL_1:8;
then
(Partial_Sums (abs seq1)) . M1 >= (Partial_Sums (abs seq1)) . n1
by A14, Th57;
then
((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1) <= ((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)
by XREAL_1:10;
then A26:
r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) <= r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1))
by A11, XREAL_1:64;
consider Fr being
XFinSequence of
such that A27:
(Partial_Sums (seq1 (##) seq2)) . m = ((Sum seq2) * ((Partial_Sums seq1) . m)) - (Sum Fr)
and A28:
dom Fr = m + 1
and A29:
for
i being
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 A30:
dom absFr = dom Fr
and A31:
abs (Sum Fr) <= Sum absFr
and A32:
for
i being
Nat st
i in dom absFr holds
absFr . i = abs (Fr . i)
by Th55;
A33:
M <= M + M
by NAT_1:11;
then A34:
M <= m
by A22, XXREAL_0:2;
then
M < len absFr
by A28, A30, NAT_1:13;
then A35:
len (absFr | M) = M
by AFINSQ_1:11;
n1 + 1
<= M
by A25, A21, XXREAL_0:2;
then
n1 + 1
<= m
by A34, XXREAL_0:2;
then A36:
n1 <= m
by NAT_1:13;
then
(Partial_Sums (abs seq1)) . m >= (Partial_Sums (abs seq1)) . n1
by A14, Th57;
then
((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1) >= ((Partial_Sums (abs seq1)) . n1) - ((Partial_Sums (abs seq1)) . n1)
by XREAL_1:9;
then A37:
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;
consider Fr1 being
XFinSequence of
such that A38:
absFr = (absFr | M) ^ Fr1
by Th5;
A39:
m + 1
= (len (absFr | M)) + (len Fr1)
by A28, A30, A38, AFINSQ_1:def 3;
then A40:
Fr1 | ((m - M) + 1) = Fr1
by A35, RELAT_1:69;
A41:
n2 <= max (
(n1 + 1),
n2)
by XXREAL_0:25;
then
n2 <= M
by A21, XXREAL_0:2;
then
n2 <= 2M
by A33, XXREAL_0:2;
then
(
n2 <= m &
m in NAT )
by A22, XXREAL_0:2;
then A42:
abs (((Partial_Sums seq2) . m) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1))
by A19;
defpred S1[
Nat]
means (
(M + $1) + 1
<= m + 1 implies
Sum (Fr1 | ($1 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + $1)) - ((Partial_Sums (abs seq1)) . M1)) );
A43:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A44:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
set Mk1 =
M + (k + 1);
A45:
abs (seq1 . (M + (k + 1))) = (abs seq1) . (M + (k + 1))
by SEQ_1:12;
assume A46:
(M + (k + 1)) + 1
<= m + 1
;
Sum (Fr1 | ((k + 1) + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + (k + 1))) - ((Partial_Sums (abs seq1)) . M1))
then A47:
M + (k + 1) < m + 1
by NAT_1:13;
then A48:
M + (k + 1) in m + 1
by NAT_1:44;
then
Fr . (M + (k + 1)) = (seq1 . (M + (k + 1))) * (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1)))
by A29;
then A49:
abs (Fr . (M + (k + 1))) = (abs (seq1 . (M + (k + 1)))) * (abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))))
by COMPLEX1:65;
M + (k + 1) < m + 1
by A46, NAT_1:13;
then
k + 1
< len Fr1
by A39, A35, XREAL_1:7;
then
k + 1
in len Fr1
by NAT_1:44;
then A50:
Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1)))
by AFINSQ_2:65;
m + 1
= len absFr
by A28, A30;
then
absFr . (M + (k + 1)) = Fr1 . ((M + (k + 1)) - M)
by A38, A35, A47, AFINSQ_1:19, NAT_1:11;
then A51:
Fr1 . (k + 1) = abs (Fr . (M + (k + 1)))
by A28, A30, A32, A48;
(
abs (seq1 . (M + (k + 1))) >= 0 &
abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))) < r )
by A12, COMPLEX1:46;
then
Fr1 . (k + 1) <= r * (abs (seq1 . (M + (k + 1))))
by A51, A49, XREAL_1:64;
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 A44, A46, A50, A45, NAT_1:13, XREAL_1:7;
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))
;
verum
end;
abs (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) < e / (3 * r)
by A20, A36;
then
r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) <= r * (e / (3 * r))
by A11, A37, XREAL_1:64;
then A52:
r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) <= r * (e / (3 * r))
by A26, XXREAL_0:2;
A53:
(
m = M + (m - M) &
m - M = m -' M )
by A22, A33, XREAL_1:233, XXREAL_0:2;
A54:
S1[
0 ]
proof
assume A55:
(M + 0) + 1
<= m + 1
;
Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0)) - ((Partial_Sums (abs seq1)) . M1))
then A56:
M < m + 1
by NAT_1:13;
then A57:
M in m + 1
by NAT_1:44;
then A58:
Fr . M = (seq1 . M) * (Sum (seq2 ^\ ((m -' M) + 1)))
by A29;
(M + 1) - M <= (m + 1) - M
by A55, XREAL_1:9;
then
1
c= len Fr1
by A39, A35, NAT_1:39;
then A59:
dom (Fr1 | 1) = 1
by RELAT_1:62;
m + 1
= len absFr
by A28, A30;
then
absFr . M = Fr1 . (M - M)
by A38, A35, A56, AFINSQ_1:19;
then
Fr1 . 0 = abs (Fr . M)
by A28, A30, A32, A57;
then A60:
Fr1 . 0 = (abs (seq1 . M)) * (abs (Sum (seq2 ^\ ((m -' M) + 1))))
by A58, COMPLEX1:65;
A61:
(
abs (seq1 . M) >= 0 &
r > abs (Sum (seq2 ^\ ((m -' M) + 1))) )
by A12, COMPLEX1:46;
0 in 1
by NAT_1:44;
then A62:
(Fr1 | 1) . 0 = Fr1 . 0
by A59, FUNCT_1:47;
((Partial_Sums (abs seq1)) . M1) + ((abs seq1) . (M1 + 1)) = (Partial_Sums (abs seq1)) . (M1 + 1)
by SERIES_1:def 1;
then A63:
((Partial_Sums (abs seq1)) . M) - ((Partial_Sums (abs seq1)) . M1) = abs (seq1 . M)
by SEQ_1:12;
Sum (Fr1 | 1) = (Fr1 | 1) . 0
by A59, Lm4;
hence
Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0)) - ((Partial_Sums (abs seq1)) . M1))
by A62, A60, A63, A61, XREAL_1:64;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A54, A43);
then
Sum Fr1 <= r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1))
by A40, A53;
then
Sum Fr1 <= r * (e / (3 * r))
by A52, XXREAL_0:2;
then A64:
Sum Fr1 <= e / 3
by A11, XCMPLX_1:92;
(abs seq1) . 0 >= 0
by A14;
then A65:
((abs seq1) . 0) * (abs (((Partial_Sums seq2) . m) - (Sum seq2))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((abs seq1) . 0)
by A42, XREAL_1:64;
A66:
0 in m + 1
by NAT_1:44;
then A67:
Fr . 0 = (seq1 . 0) * (Sum (seq2 ^\ ((m -' 0) + 1)))
by A29;
(Partial_Sums (abs seq1)) . M1 <= Sum (abs seq1)
by A15, A16, RSSPACE2:3;
then A68:
(e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum (abs seq1))
by A5, A18, 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 A23, XXREAL_0:2;
then
(
n0 <= m &
m in NAT )
by A34, XXREAL_0:2;
then A70:
abs (((Partial_Sums seq1) . m) - (Sum seq1)) < e / (3 * ((abs (Sum seq2)) + 1))
by A7;
(
abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) = (abs (Sum seq2)) * (abs (((Partial_Sums seq1) . m) - (Sum seq1))) &
abs (Sum seq2) >= 0 )
by COMPLEX1:46, COMPLEX1:65;
then A71:
abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) <= (abs (Sum seq2)) * (e / (3 * ((abs (Sum seq2)) + 1)))
by A70, XREAL_1:64;
A72:
Sum absFr = (Sum (absFr | M)) + (Sum Fr1)
by A38, AFINSQ_2:55;
defpred S2[
Nat]
means ( $1
+ 1
<= M implies
Sum (absFr | ($1 + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . $1) );
A73:
n2 <= M
by A41, A21, XXREAL_0:2;
A74:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A75:
S2[
k]
;
S2[k + 1]
reconsider k1 =
k + 1 as
Element of
NAT ;
A76:
abs (seq1 . k1) = (abs seq1) . k1
by SEQ_1:12;
A77:
m - M >= 2M - M
by A22, XREAL_1:9;
assume A78:
(k + 1) + 1
<= M
;
Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs 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))) * (abs (seq1 . k1))) + (Sum (absFr | k1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))) + ((e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . k))
by A75, A78, NAT_1:13, XREAL_1:6;
then
(
((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))) + (Sum (absFr | k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (((abs seq1) . k1) + ((Partial_Sums (abs seq1)) . k)) &
k in NAT )
by A76, ORDINAL1:def 12;
then A81:
((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))) + (Sum (absFr | k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . k1)
by SERIES_1:def 1;
k1 < m
by A34, A79, XXREAL_0:2;
then
k1 < m + 1
by NAT_1:13;
then A82:
k1 in m + 1
by NAT_1:44;
then A83:
Sum (absFr | (k1 + 1)) = (absFr . k1) + (Sum (absFr | k1))
by A28, A30, AFINSQ_2:65;
m - k1 = m -' k1
by A34, A79, XREAL_1:233, XXREAL_0:2;
then
abs (((Partial_Sums seq2) . (m -' k1)) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1))
by A19, A80;
then A84:
abs ((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;
abs (seq1 . k1) >= 0
by COMPLEX1:46;
then
(abs ((Sum seq2) - ((Partial_Sums seq2) . (m -' k1)))) * (abs (seq1 . k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))
by A84, XREAL_1:64;
then A86:
abs ((seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1)))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))
by A85, COMPLEX1:65;
(
Fr . k1 = (seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1))) &
abs (Fr . k1) = absFr . k1 )
by A28, A29, A30, A32, A82;
then
Sum (absFr | (k1 + 1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (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 (abs seq1)) . (k + 1))
by A81, XXREAL_0:2;
verum
end;
(
Sum (absFr | (0 + 1)) = (absFr . 0) + (Sum (absFr | 0)) &
absFr . 0 = abs (Fr . 0) )
by A28, A30, A32, A66, AFINSQ_2:65;
then Sum (absFr | (0 + 1)) =
(abs (seq1 . 0)) * (abs (Sum (seq2 ^\ ((m -' 0) + 1))))
by A67, COMPLEX1:65
.=
((abs seq1) . 0) * (abs (Sum (seq2 ^\ ((m -' 0) + 1))))
by SEQ_1:12
.=
((abs seq1) . 0) * (abs (((Partial_Sums seq2) . m) - (Sum seq2)))
by A69, COMPLEX1:60
;
then A87:
S2[
0 ]
by A65, SERIES_1:def 1;
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A87, A74);
then A88:
Sum (absFr | M) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1)
by A24;
(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, A18, XREAL_1:64;
then
(e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= e / 3
by A68, A17, XXREAL_0:2;
then
Sum (absFr | M) <= e / 3
by A88, XXREAL_0:2;
then
(Sum (absFr | M)) + (Sum Fr1) <= (e / 3) + (e / 3)
by A64, XREAL_1:7;
then A89:
abs (Sum Fr) <= (e / 3) + (e / 3)
by A31, A72, XXREAL_0:2;
((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2)) = ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) - (Sum Fr)
by A27;
then A90:
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) <= (abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1)))) + (abs (Sum Fr))
by COMPLEX1:57;
e / (3 * ((abs (Sum seq2)) + 1)) > 0
by A5, A6, XREAL_1:139;
then
(e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) > (e / (3 * ((abs (Sum seq2)) + 1))) * (abs (Sum seq2))
by A13, XREAL_1:68;
then
abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) < e / 3
by A9, A71, XXREAL_0:2;
then
(abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1)))) + (abs (Sum Fr)) < (e / 3) + ((e / 3) + (e / 3))
by A89, XREAL_1:8;
hence
abs (((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))) < e
by A90, XXREAL_0:2;
verum
end;
then A91:
Partial_Sums (seq1 (##) seq2) is convergent
by SEQ_2:def 6;
hence
seq1 (##) seq2 is summable
by SERIES_1:def 2; Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2)
lim (Partial_Sums (seq1 (##) seq2)) = (Sum seq1) * (Sum seq2)
by A3, A91, SEQ_2:def 7;
hence
Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2)
by SERIES_1:def 3; verum