let seq1, seq2 be Real_Sequence; :: thesis: for n being Element of NAT st seq2 is summable holds
ex Fr being XFinSequence of 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 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 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))) ) )
set S = seq1 (##) seq2;
set P1 = Partial_Sums seq1;
set P2 = Partial_Sums seq2;
defpred S₁[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1)));
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 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);
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))) ) )
consider Fr1 being XFinSequence of 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;
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) );
A8: S₂[ 0 ]

proof

( 0 in n + 1 & dom (Fr | 0 ) = {} & dom (Fr1 | 0 ) = {} ) by NAT_1:45;
then ( Sum (Fr | (0 + 1)) = (Fr . 0 ) + (Sum (Fr | 0 )) & Sum (Fr | 0 ) = 0 & Fr . 0 = (seq1 . 0 ) * (Sum (seq2 ^\ ((n -' 0 ) + 1))) & Fr1 . 0 = (seq1 . 0 ) * ((Partial_Sums seq2) . (n -' 0 )) & Sum (Fr1 | (0 + 1)) = (Fr1 . 0 ) + (Sum (Fr1 | 0 )) & Sum (Fr1 | 0 ) = 0 ) by A3, A4, A6, A7, Lm6, Lm8;
then (Sum (Fr | (0 + 1))) + (Sum (Fr1 | (0 + 1))) = (seq1 . 0 ) * ((Sum (seq2 ^\ ((n -' 0 ) + 1))) + ((Partial_Sums seq2) . (n -' 0 )))
.= (seq1 . 0 ) * (Sum seq2) by A1, SERIES_1:18 ;
hence S₂[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A9: 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 A10: S₂[k] ; :: thesis: S₂[k + 1]
set k1 = k + 1;
assume (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 & k + 1 <= (k + 1) + 1 ) by NAT_1:13;
then ( k + 1 in n + 1 & k + 1 <= n + 1 ) by NAT_1:45;
then ( Sum (Fr | ((k + 1) + 1)) = (Fr . (k + 1)) + (Sum (Fr | (k + 1))) & Fr1 . (k + 1) = (seq1 . (k + 1)) * ((Partial_Sums seq2) . (n -' (k + 1))) & Fr . (k + 1) = (seq1 . (k + 1)) * (Sum (seq2 ^\ ((n -' (k + 1)) + 1))) & Sum (Fr1 | ((k + 1) + 1)) = (Fr1 . (k + 1)) + (Sum (Fr1 | (k + 1))) & (Sum (Fr1 | (k + 1))) + (Sum (Fr | (k + 1))) = (Sum seq2) * ((Partial_Sums seq1) . k) ) by A3, A4, A6, A7, A10, 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))
.= ((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;

A11: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A8, A9);
( Fr | (n + 1) = Fr & Fr1 | (n + 1) = Fr1 ) by A3, A6, RELAT_1:98;
then (Sum Fr1) + (Sum Fr) = (Sum seq2) * ((Partial_Sums seq1) . n) by A11;
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