let seq1, seq2 be Real_Sequence; :: thesis: for n being Element of 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 Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
let n be Element of 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 Element of 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 Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
defpred S₁[ set , set ] means for i being Element of 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 Element of NAT st i in n + 1 holds
ex x being Element of REAL st S₁[i,x]

proof

let i be Element of NAT ; :: thesis: ( i in n + 1 implies ex x being Element of REAL st S₁[i,x] )
assume i in n + 1 ; :: thesis: ex x being Element of REAL st S₁[i,x]
take (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ; :: thesis: S₁[i,(seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1)))]
thus S₁[i,(seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1)))] ; :: thesis: verum

end;

consider Fr being XFinSequence of REAL such that
A3: dom Fr = n + 1 and
A4: for i being Element of NAT st i in n + 1 holds
S₁[i,Fr . i] from STIRL2_1:sch 6(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 Element of NAT st i in n + 1 holds
Fr1 . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) by Th53;
A8: 0 in n + 1 by NAT_1:45;
then A9: ( Fr1 . 0 = (seq1 . 0 ) * ((Partial_Sums seq2) . (n -' 0 )) & Sum (Fr1 | (0 + 1)) = (Fr1 . 0 ) + (Sum (Fr1 | 0 )) ) by A6, A7, Lm8;
defpred S₂[ Element of 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 Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A11: S₂[k] ; :: thesis: S₂[k + 1]
set k1 = k + 1;
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 k + 1 < n + 1 by NAT_1:13;
then A13: k + 1 in n + 1 by NAT_1:45;
then A14: ( Fr . (k + 1) = (seq1 . (k + 1)) * (Sum (seq2 ^\ ((n -' (k + 1)) + 1))) & Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1))) ) by A4, A6, Lm8;
( Sum (Fr | ((k + 1) + 1)) = (Fr . (k + 1)) + (Sum (Fr | (k + 1))) & Fr1 . (k + 1) = (seq1 . (k + 1)) * ((Partial_Sums seq2) . (n -' (k + 1))) ) by A3, A7, A13, Lm8;
then (Sum (Fr | ((k + 1) + 1))) + (Sum (Fr1 | ((k + 1) + 1))) = ((seq1 . (k + 1)) * ((Sum (seq2 ^\ ((n -' (k + 1)) + 1))) + ((Partial_Sums seq2) . (n -' (k + 1))))) + ((Sum seq2) * ((Partial_Sums seq1) . k)) by A11, A12, A14, NAT_1:13
.= ((seq1 . (k + 1)) * (Sum seq2)) + ((Sum seq2) * ((Partial_Sums seq1) . k)) by A1, SERIES_1:18
.= (Sum seq2) * (((Partial_Sums seq1) . k) + (seq1 . (k + 1)))
.= ((Partial_Sums seq1) . (k + 1)) * (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;

dom (Fr | 0 ) = {} ;
then A15: Sum (Fr | 0 ) = 0 by Lm6;
( Sum (Fr | (0 + 1)) = (Fr . 0 ) + (Sum (Fr | 0 )) & Fr . 0 = (seq1 . 0 ) * (Sum (seq2 ^\ ((n -' 0 ) + 1))) ) by A3, A4, A8, Lm8;
then (Sum (Fr | (0 + 1))) + (Sum (Fr1 | (0 + 1))) = (seq1 . 0 ) * ((Sum (seq2 ^\ ((n -' 0 ) + 1))) + ((Partial_Sums seq2) . (n -' 0 ))) by A15, A9
.= (seq1 . 0 ) * (Sum seq2) by A1, SERIES_1:18 ;
then A16: S₂[ 0 ] by SERIES_1:def 1;
A17: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A16, A10);
take Fr ; :: thesis: ( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )
A18: Fr1 | (n + 1) = Fr1 by A6, RELAT_1:98;
Fr | (n + 1) = Fr by A3, RELAT_1:98;
then (Sum Fr1) + (Sum Fr) = (Sum seq2) * ((Partial_Sums seq1) . n) by A17, A18;
hence ( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) ) by A3, A4, A5; :: thesis: verum