let seq1, seq2 be Real_Sequence; for n being Nat st seq2 is summable holds
ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
let n be Nat; ( seq2 is summable implies ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) ) )
assume A1:
seq2 is summable
; ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
defpred S1[ set , set ] means for i being Nat st i = $1 holds
$2 = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1)));
set P2 = Partial_Sums seq2;
set P1 = Partial_Sums seq1;
set S = seq1 (##) seq2;
A2:
for i being Nat st i in Segm (n + 1) holds
ex x being Element of REAL st S1[i,x]
consider Fr being XFinSequence of REAL such that
A3:
dom Fr = Segm (n + 1)
and
A4:
for i being Nat st i in Segm (n + 1) holds
S1[i,Fr . i]
from STIRL2_1:sch 5(A2);
consider Fr1 being XFinSequence of REAL such that
A5:
(Partial_Sums (seq1 (##) seq2)) . n = Sum Fr1
and
A6:
dom Fr1 = n + 1
and
A7:
for i being Nat st i in n + 1 holds
Fr1 . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i))
by Th48;
A8:
0 in Segm (n + 1)
by NAT_1:44;
then A9:
( Fr1 . 0 = (seq1 . 0) * ((Partial_Sums seq2) . (n -' 0)) & Sum (Fr1 | (zz + 1)) = (Fr1 . 0) + (Sum (Fr1 | zz)) )
by A6, A7, AFINSQ_2:65;
defpred S2[ Nat] means ( $1 + 1 <= n + 1 implies (Sum (Fr1 | ($1 + 1))) + (Sum (Fr | ($1 + 1))) = (Sum seq2) * ((Partial_Sums seq1) . $1) );
A10:
for k being Nat st S2[k] holds
S2[k + 1]
A16:
Sum (Fr | zz) = 0
;
A17:
Sum (Fr1 | zz) = 0
;
A18:
( Sum (Fr | (zz + 1)) = (Fr . 0) + (Sum (Fr | zz)) & Fr . 0 = (seq1 . 0) * (Sum (seq2 ^\ ((n -' 0) + 1))) )
by A3, A4, A8, AFINSQ_2:65;
then (Sum (Fr | (zz + 1))) + (Sum (Fr1 | (zz + 1))) =
((Fr . 0) + (Sum (Fr | zz))) + (Sum (Fr1 | (zz + 1)))
.=
(Fr . 0) + (Sum (Fr1 | (zz + 1)))
by A16
.=
((seq1 . 0) * (Sum (seq2 ^\ ((n -' 0) + 1)))) + (Sum (Fr1 | (zz + 1)))
by A18
.=
(((seq1 . 0) * (Sum (seq2 ^\ ((n -' 0) + 1)))) + (Fr1 . 0)) + (Sum (Fr1 | zz))
by A9
.=
(((seq1 . 0) * (Sum (seq2 ^\ ((n -' 0) + 1)))) + ((seq1 . 0) * ((Partial_Sums seq2) . (n -' 0)))) + (Sum (Fr1 | zz))
by A9
.=
(seq1 . 0) * ((Sum (seq2 ^\ ((n -' 0) + 1))) + ((Partial_Sums seq2) . (n -' 0)))
by A17
.=
(seq1 . 0) * (Sum seq2)
by A1, SERIES_1:15
;
then A19:
S2[ 0 ]
by SERIES_1:def 1;
A20:
for k being Nat holds S2[k]
from NAT_1:sch 2(A19, A10);
take
Fr
; ( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
A21:
Fr1 | (n + 1) = Fr1
by A6;
Fr | (n + 1) = Fr
by A3;
then
(Sum Fr1) + (Sum Fr) = (Sum seq2) * ((Partial_Sums seq1) . n)
by A20, A21;
hence
( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
by A3, A4, A5; verum