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 |.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;
( 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
;
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;
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;
for m being Nat st 2M <= m holds
|.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e
let m be
Nat;
( 2M <= m implies |.(((Partial_Sums (seq1 (##) seq2)) . m) - ((Sum seq1) * (Sum seq2))).| < e )
assume A21:
2M <= m
;
|.(((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 S1[
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
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A43:
S1[
k]
;
S1[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
;
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))
;
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:
S1[
0 ]
proof
assume A55:
(M + 0) + 1
<= m + 1
;
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;
verum
end;
for
k being
Nat holds
S1[
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 S2[
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
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
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
;
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;
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:
S2[
0 ]
by A65, SERIES_1:def 1;
for
k being
Nat holds
S2[
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;
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; 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; verum