let seq1, seq2 be Real_Sequence; :: thesis: for n being 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 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 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 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 n + 1 holds
ex x being Element of REAL st S₁[i,x]

proof

let i be 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 Nat st i in n + 1 holds
S₁[i,Fr . i] from STIRL2_1:sch 5(A2);
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 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, AFINSQ_2:77;
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 Element of NAT ;
assume BB: (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 n + 1 by NAT_1:45;
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:77;
B15: (Sum (Fr1 | k1)) + (Sum (Fr | k1)) = (Sum seq2) * ((Partial_Sums seq1) . k) by BB, NAT_1:13, A11;
B: k in NAT by ORDINAL1:def 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:77;
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 B15, A14
.= ((seq1 . k1) * (Sum seq2)) + ((Sum seq2) * ((Partial_Sums seq1) . k)) by A1, SERIES_1:18
.= (Sum seq2) * (((Partial_Sums seq1) . k) + (seq1 . k1))
.= ((Partial_Sums seq1) . k1) * (Sum seq2) by SERIES_1:def 1, B ;
hence (Sum (Fr1 | ((k + 1) + 1))) + (Sum (Fr | ((k + 1) + 1))) = (Sum seq2) * ((Partial_Sums seq1) . (k + 1)) ; :: thesis: verum

end;

( Sum (Fr | (0 + 1)) = (Fr . 0) + (Sum (Fr | 0)) & Fr . 0 = (seq1 . 0) * (Sum (seq2 ^\ ((n -' 0) + 1))) ) by A3, A4, A8, AFINSQ_2:77;
then (Sum (Fr | (0 + 1))) + (Sum (Fr1 | (0 + 1))) = (seq1 . 0) * ((Sum (seq2 ^\ ((n -' 0) + 1))) + ((Partial_Sums seq2) . (n -' 0))) by A9
.= (seq1 . 0) * (Sum seq2) by A1, SERIES_1:18 ;
then A16: S₂[ 0 ] by SERIES_1:def 1;
A17: for k being Nat holds S₂[k] from NAT_1:sch 2(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 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 Nat st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) ) by A3, A4, A5; :: thesis: verum