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:40;
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:132, XREAL_1:10;
then A6:
3
* ((abs (Sum seq2)) + 1) > 3
* 0
by XREAL_1:70;
then
(
lim (Partial_Sums seq1) = Sum seq1 &
e / (3 * ((abs (Sum seq2)) + 1)) > 0 )
by A5, SERIES_1:def 3, XREAL_1:141;
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:132, XREAL_1:10;
then A9:
(e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) = e / 3
by XCMPLX_1:93;
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:10;
then B14:
for
n being
Element of
NAT holds
(abs seq1) . n >= 0
;
A15:
abs seq1 is
summable
by A1, SERIES_1:def 5;
then
Sum (abs seq1) >= 0
by SERIES_1:21, B14;
then A16:
((Sum (abs seq1)) + 1) * (e / (3 * ((Sum (abs seq1)) + 1))) = e / 3
by XCMPLX_1:93;
A17:
Sum (abs seq1) >= 0
by A15, SERIES_1:21, B14;
then
3
* ((Sum (abs seq1)) + 1) > 0 * 3
by XREAL_1:70;
then
e / (3 * ((Sum (abs seq1)) + 1)) > 0
by A5, XREAL_1:141;
then consider n2 being
Element of
NAT such that A18:
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:70;
then
e / (3 * r) > 0
by A5, XREAL_1:141;
then consider n1 being
Element of
NAT such that A19:
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 A15, SERIES_1:25;
(
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;
A20:
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 A21:
2M <= m
;
abs (((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
Element of
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:10;
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:12;
then A25:
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:66;
consider Fr being
XFinSequence of
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, Th54;
consider absFr being
XFinSequence of
such that A29:
dom absFr = dom Fr
and A30:
abs (Sum Fr) <= Sum absFr
and A31:
for
i being
Nat st
i in dom absFr holds
absFr . i = abs (Fr . i)
by Th55;
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:14;
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 (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:11;
then A36:
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 A37:
absFr = (absFr | M) ^ Fr1
by Th5;
A38:
m + 1
= (len (absFr | M)) + (len Fr1)
by A27, A29, A37, AFINSQ_1:def 4;
then A39:
Fr1 | ((m - M) + 1) = Fr1
by A34, RELAT_1:98;
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;
then A41:
abs (((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 (abs seq1)) . (M + $1)) - ((Partial_Sums (abs 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);
A44:
abs (seq1 . (M + (k + 1))) = (abs seq1) . (M + (k + 1))
by SEQ_1:16;
assume A45:
(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 A46:
M + (k + 1) < m + 1
by NAT_1:13;
then A47:
M + (k + 1) in m + 1
by NAT_1:45;
then
Fr . (M + (k + 1)) = (seq1 . (M + (k + 1))) * (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1)))
by A28;
then A48:
abs (Fr . (M + (k + 1))) = (abs (seq1 . (M + (k + 1)))) * (abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))))
by COMPLEX1:151;
M + (k + 1) < m + 1
by A45, NAT_1:13;
then
k + 1
< len Fr1
by A38, A34, XREAL_1:9;
then
k + 1
in len Fr1
by NAT_1:45;
then A49:
Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1)))
by AFINSQ_2:77;
m + 1
= len absFr
by A27, A29;
then
absFr . (M + (k + 1)) = Fr1 . ((M + (k + 1)) - M)
by A37, A34, A46, AFINSQ_1:22, NAT_1:11;
then A50:
Fr1 . (k + 1) = abs (Fr . (M + (k + 1)))
by A27, A29, A31, A47;
(
abs (seq1 . (M + (k + 1))) >= 0 &
abs (Sum (seq2 ^\ ((m -' (M + (k + 1))) + 1))) < r )
by A12, COMPLEX1:132;
then
Fr1 . (k + 1) <= r * (abs (seq1 . (M + (k + 1))))
by A50, A48, XREAL_1:66;
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 A43, A45, A49, A44, NAT_1:13, 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))
;
verum
end;
abs (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) < e / (3 * r)
by A19, A35;
then
r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . n1)) <= r * (e / (3 * r))
by A11, A36, XREAL_1:66;
then A51:
r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1)) <= r * (e / (3 * r))
by A25, XXREAL_0:2;
A52:
(
m = M + (m - M) &
m - M = m -' M )
by A21, A32, XREAL_1:235, XXREAL_0:2;
A53:
S1[
0 ]
proof
assume A54:
(M + 0) + 1
<= m + 1
;
Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0)) - ((Partial_Sums (abs seq1)) . M1))
then A55:
M < m + 1
by NAT_1:13;
then A56:
M in m + 1
by NAT_1:45;
then A57:
Fr . M = (seq1 . M) * (Sum (seq2 ^\ ((m -' M) + 1)))
by A28;
(M + 1) - M <= (m + 1) - M
by A54, XREAL_1:11;
then
1
c= len Fr1
by A38, A34, NAT_1:40;
then A58:
dom (Fr1 | 1) = 1
by RELAT_1:91;
m + 1
= len absFr
by A27, A29;
then
absFr . M = Fr1 . (M - M)
by A37, A34, A55, AFINSQ_1:22;
then
Fr1 . 0 = abs (Fr . M)
by A27, A29, A31, A56;
then A59:
Fr1 . 0 = (abs (seq1 . M)) * (abs (Sum (seq2 ^\ ((m -' M) + 1))))
by A57, COMPLEX1:151;
A60:
(
abs (seq1 . M) >= 0 &
r > abs (Sum (seq2 ^\ ((m -' M) + 1))) )
by A12, COMPLEX1:132;
0 in 1
by NAT_1:45;
then A61:
(Fr1 | 1) . 0 = Fr1 . 0
by A58, FUNCT_1:70;
((Partial_Sums (abs seq1)) . M1) + ((abs seq1) . (M1 + 1)) = (Partial_Sums (abs seq1)) . (M1 + 1)
by SERIES_1:def 1;
then A62:
((Partial_Sums (abs seq1)) . M) - ((Partial_Sums (abs seq1)) . M1) = abs (seq1 . M)
by SEQ_1:16;
Sum (Fr1 | 1) = (Fr1 | 1) . 0
by A58, Lm7;
hence
Sum (Fr1 | (0 + 1)) <= r * (((Partial_Sums (abs seq1)) . (M + 0)) - ((Partial_Sums (abs seq1)) . M1))
by A61, A59, A62, A60, XREAL_1:66;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A53, A42);
then
Sum Fr1 <= r * (((Partial_Sums (abs seq1)) . m) - ((Partial_Sums (abs seq1)) . M1))
by A39, A52;
then
Sum Fr1 <= r * (e / (3 * r))
by A51, XXREAL_0:2;
then A63:
Sum Fr1 <= e / 3
by A11, XCMPLX_1:93;
(abs seq1) . 0 >= 0
by A14;
then A64:
((abs seq1) . 0) * (abs (((Partial_Sums seq2) . m) - (Sum seq2))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((abs seq1) . 0)
by A41, XREAL_1:66;
A65:
0 in m + 1
by NAT_1:45;
then A66:
Fr . 0 = (seq1 . 0) * (Sum (seq2 ^\ ((m -' 0) + 1)))
by A28;
(Partial_Sums (abs seq1)) . M1 <= Sum (abs seq1)
by B14, A15, RSSPACE2:4;
then A67:
(e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (Sum (abs seq1))
by A5, A17, XREAL_1:66;
(
Sum seq2 = ((Partial_Sums seq2) . (m -' 0)) + (Sum (seq2 ^\ ((m -' 0) + 1))) &
m -' 0 = m )
by A2, NAT_D:40, SERIES_1:18;
then A68:
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;
then A69:
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:132, COMPLEX1:151;
then A70:
abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) <= (abs (Sum seq2)) * (e / (3 * ((abs (Sum seq2)) + 1)))
by A69, XREAL_1:66;
A71:
Sum absFr = (Sum (absFr | M)) + (Sum Fr1)
by A37, AFINSQ_2:67;
defpred S2[
Nat]
means ( $1
+ 1
<= M implies
Sum (absFr | ($1 + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . $1) );
A72:
n2 <= M
by A40, A20, XXREAL_0:2;
A73:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A74:
S2[
k]
;
S2[k + 1]
reconsider k1 =
k + 1 as
Element of
NAT ;
A75:
abs (seq1 . k1) = (abs seq1) . k1
by SEQ_1:16;
A76:
m - M >= 2M - M
by A21, XREAL_1:11;
assume A77:
(k + 1) + 1
<= M
;
Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . (k + 1))
then A78:
k1 < M
by NAT_1:13;
then
m - k1 >= m - M
by XREAL_1:12;
then
m - k1 >= M
by A76, XXREAL_0:2;
then A79:
m - k1 >= n2
by A72, 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 A74, A77, NAT_1:13, XREAL_1:8;
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 A75, ORDINAL1:def 13;
then A80:
((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 A33, A78, XXREAL_0:2;
then
k1 < m + 1
by NAT_1:13;
then A81:
k1 in m + 1
by NAT_1:45;
then A82:
Sum (absFr | (k1 + 1)) = (absFr . k1) + (Sum (absFr | k1))
by A27, A29, AFINSQ_2:77;
m - k1 = m -' k1
by A33, A78, XREAL_1:235, XXREAL_0:2;
then
abs (((Partial_Sums seq2) . (m -' k1)) - (Sum seq2)) < e / (3 * ((Sum (abs seq1)) + 1))
by A18, A79;
then A83:
abs ((Sum seq2) - ((Partial_Sums seq2) . (m -' k1))) < e / (3 * ((Sum (abs seq1)) + 1))
by COMPLEX1:146;
A84:
Sum seq2 = ((Partial_Sums seq2) . (m -' k1)) + (Sum (seq2 ^\ ((m -' k1) + 1)))
by A2, SERIES_1:18;
abs (seq1 . k1) >= 0
by COMPLEX1:132;
then
(abs ((Sum seq2) - ((Partial_Sums seq2) . (m -' k1)))) * (abs (seq1 . k1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))
by A83, XREAL_1:66;
then A85:
abs ((seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1)))) <= (e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))
by A84, COMPLEX1:151;
(
Fr . k1 = (seq1 . k1) * (Sum (seq2 ^\ ((m -' k1) + 1))) &
abs (Fr . k1) = absFr . k1 )
by A27, A28, A29, A31, A81;
then
Sum (absFr | (k1 + 1)) <= ((e / (3 * ((Sum (abs seq1)) + 1))) * (abs (seq1 . k1))) + (Sum (absFr | k1))
by A82, A85, XREAL_1:8;
hence
Sum (absFr | ((k + 1) + 1)) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . (k + 1))
by A80, XXREAL_0:2;
verum
end;
(
Sum (absFr | (0 + 1)) = (absFr . 0) + (Sum (absFr | 0)) &
absFr . 0 = abs (Fr . 0) )
by A27, A29, A31, A65, AFINSQ_2:77;
then Sum (absFr | (0 + 1)) =
(abs (seq1 . 0)) * (abs (Sum (seq2 ^\ ((m -' 0) + 1))))
by A66, 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 A68, COMPLEX1:146
;
then A87:
S2[
0 ]
by A64, SERIES_1:def 1;
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A87, A73);
then A88:
Sum (absFr | M) <= (e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1)
by A23;
(Sum (abs seq1)) + 1
> (Sum (abs seq1)) + 0
by XREAL_1:10;
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:66;
then
(e / (3 * ((Sum (abs seq1)) + 1))) * ((Partial_Sums (abs seq1)) . M1) <= e / 3
by A67, A16, 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 A63, XREAL_1:9;
then A89:
abs (Sum Fr) <= (e / 3) + (e / 3)
by A30, A71, 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 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:143;
e / (3 * ((abs (Sum seq2)) + 1)) > 0
by A5, A6, XREAL_1:141;
then
(e / (3 * ((abs (Sum seq2)) + 1))) * ((abs (Sum seq2)) + 1) > (e / (3 * ((abs (Sum seq2)) + 1))) * (abs (Sum seq2))
by A13, XREAL_1:70;
then
abs ((Sum seq2) * (((Partial_Sums seq1) . m) - (Sum seq1))) < e / 3
by A9, A70, 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:10;
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