let seq1, seq2 be Real_Sequence; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 S₁[i,x]

proof

let i be Nat; :: thesis: ( i in Segm (n + 1) implies ex x being Element of REAL st S₁[i,x] )
assume i in Segm (n + 1) ; :: thesis: ex x being Element of REAL st S₁[i,x]
reconsider ss = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) as Element of REAL by XREAL_0:def 1;
take ss ; :: thesis: S₁[i,ss]
thus S₁[i,ss] ; :: thesis: verum

end;

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
S₁[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 S₂[ 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 S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A11: S₂[k] ; :: thesis: S₂[k + 1]
reconsider k1 = k + 1 as Nat ;
assume A12: (k + 1) + 1 <= n + 1 ; :: thesis: (Sum (Fr1 | ((k + 1) + 1))) + (Sum (Fr | ((k + 1) + 1))) = (Sum seq2) * ((Partial_Sums seq1) . (k + 1))
then k1 < n + 1 by NAT_1:13;
then A13: k1 in Segm (n + 1) by NAT_1:44;
then A14: ( Fr . k1 = (seq1 . k1) * (Sum (seq2 ^\ ((n -' k1) + 1))) & Sum (Fr1 | (k1 + 1)) = (Fr1 . k1) + (Sum (Fr1 | k1)) ) by A4, A6, AFINSQ_2:65;
A15: (Sum (Fr1 | k1)) + (Sum (Fr | k1)) = (Sum seq2) * ((Partial_Sums seq1) . k) by A12, A11, NAT_1:13;
( Sum (Fr | (k1 + 1)) = (Fr . k1) + (Sum (Fr | k1)) & Fr1 . k1 = (seq1 . k1) * ((Partial_Sums seq2) . (n -' k1)) ) by A3, A7, A13, AFINSQ_2:65;
then (Sum (Fr | (k1 + 1))) + (Sum (Fr1 | (k1 + 1))) = ((seq1 . k1) * ((Sum (seq2 ^\ ((n -' k1) + 1))) + ((Partial_Sums seq2) . (n -' k1)))) + ((Sum seq2) * ((Partial_Sums seq1) . k)) by A15, A14
.= ((seq1 . k1) * (Sum seq2)) + ((Sum seq2) * ((Partial_Sums seq1) . k)) by A1, SERIES_1:15
.= (Sum seq2) * (((Partial_Sums seq1) . k) + (seq1 . k1))
.= ((Partial_Sums seq1) . k1) * (Sum seq2) by SERIES_1:def 1 ;
hence (Sum (Fr1 | ((k + 1) + 1))) + (Sum (Fr | ((k + 1) + 1))) = (Sum seq2) * ((Partial_Sums seq1) . (k + 1)) ; :: thesis: verum

end;

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: S₂[ 0 ] by SERIES_1:def 1;
A20: for k being Nat holds S₂[k] from NAT_1:sch 2(A19, A10);
take Fr ; :: thesis: ( (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; :: thesis: verum