let seq1, seq2 be Real_Sequence; :: thesis:
let n be Nat; :: thesis:
set S = seq1 (##) seq2;
set P = Partial_Sums seq2;
defpred S₁[ Nat] means ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . $1 = Sum Fr & dom Fr = $1 + 1 & ( for i being Nat st i in $1 + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . ($1 -' i)) ) );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

set A = addreal ;
let n be Nat; :: thesis:
set n1 = n + 1;
defpred S₂[ set , set ] means for i being Nat st i = $1 holds
$2 = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i));
A2: ( (n + 1) -' (n + 1) = 0 & (Partial_Sums seq2) . 0 = seq2 . 0 ) by SERIES_1:def 1, XREAL_1:232;
A3: for i being Nat st i in Segm ((n + 1) + 1) holds
ex x being Element of REAL st S₂[i,x]

let i be Nat; :: thesis:
assume i in Segm ((n + 1) + 1) ; :: thesis:
reconsider ss = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) as Element of REAL ;
take ss ; :: thesis:
thus S₂[i,ss] ; :: thesis:

end;

consider Fr2 being XFinSequence of REAL such that
A4: dom Fr2 = Segm ((n + 1) + 1) and
A5: for i being Nat st i in Segm ((n + 1) + 1) holds
S₂[i,Fr2 . i] from STIRL2_1:sch 5(A3);
assume S₁[n] ; :: thesis:
then consider Fr being XFinSequence of REAL such that
A6: (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr and
A7: dom Fr = n + 1 and
A8: for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ;
consider Fr1 being XFinSequence of REAL such that
A9: dom Fr1 = (n + 1) + 1 and
A10: for i being Nat st i in (n + 1) + 1 holds
Fr1 . i = (seq1 . i) * (seq2 . ((n + 1) -' i)) and
A11: Sum Fr1 = (seq1 (##) seq2) . (n + 1) by Def4;
A12: Fr1 | ((n + 1) + 1) = Fr1 by A9;
A13: for i being Nat st i in dom (Fr2 | (n + 1)) holds
(Fr2 | (n + 1)) . i = addreal . ((Fr . i),((Fr1 | (n + 1)) . i))

let i be Nat; :: thesis:
assume A14: i in dom (Fr2 | (n + 1)) ; :: thesis:
A15: i in (dom Fr2) /\ (n + 1) by A14, RELAT_1:61;
then i in dom (Fr1 | (n + 1)) by A9, A4, RELAT_1:61;
then A16: Fr1 . i = (Fr1 | (n + 1)) . i by FUNCT_1:47;
A17: i in Segm (n + 1) by A15, XBOOLE_0:def 4;
then A18: i < n + 1 by NAT_1:44;
then i <= n by NAT_1:13;
then A19: n -' i = n - i by XREAL_1:233;
( i in (n + 1) + 1 & i in NAT ) by A4, A15, XBOOLE_0:def 4;
then A20: ( Fr1 . i = (seq1 . i) * (seq2 . ((n + 1) -' i)) & Fr2 . i = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) ) by A10, A5;
A21: Fr2 . i = (Fr2 | (n + 1)) . i by A14, FUNCT_1:47;
(n + 1) -' i = (n + 1) - i by A18, XREAL_1:233;
then (n -' i) + 1 = (n + 1) -' i by A19;
then A22: (Partial_Sums seq2) . ((n + 1) -' i) = ((Partial_Sums seq2) . (n -' i)) + (seq2 . ((n + 1) -' i)) by SERIES_1:def 1;
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) by A8, A17;
then Fr2 . i = (Fr . i) + (Fr1 . i) by A20, A22;
hence (Fr2 | (n + 1)) . i = addreal . ((Fr . i),((Fr1 | (n + 1)) . i)) by A16, A21, BINOP_2:def 9; :: thesis:

end;

n + 1 <= (n + 1) + 1 by NAT_1:11;
then A23: Segm (n + 1) c= Segm ((n + 1) + 1) by NAT_1:39;
then A24: len (Fr1 | (n + 1)) = len Fr by A7, A9, RELAT_1:62;
n + 1 < (n + 1) + 1 by NAT_1:13;
then A25: n + 1 in Segm ((n + 1) + 1) by NAT_1:44;
then A26: ( Fr1 . (n + 1) = (seq1 . (n + 1)) * (seq2 . ((n + 1) -' (n + 1))) & Sum (Fr1 | ((n + 1) + 1)) = (Fr1 . (n + 1)) + (Sum (Fr1 | (n + 1))) ) by A9, A10, AFINSQ_2:65;
len (Fr2 | (n + 1)) = len Fr by A7, A4, A23, RELAT_1:62;
then addreal "**" (Fr2 | (n + 1)) = addreal "**" (Fr ^ (Fr1 | (n + 1))) by A13, A24, AFINSQ_2:46
.= Sum (Fr ^ (Fr1 | (n + 1))) by AFINSQ_2:48
.= (Sum Fr) + (Sum (Fr1 | (n + 1))) by AFINSQ_2:55 ;
then A27: Sum (Fr2 | (n + 1)) = (Sum Fr) + (Sum (Fr1 | (n + 1))) by AFINSQ_2:48;
take Fr2 ; :: thesis:
( Fr2 . (n + 1) = (seq1 . (n + 1)) * ((Partial_Sums seq2) . ((n + 1) -' (n + 1))) & Sum (Fr2 | ((n + 1) + 1)) = (Fr2 . (n + 1)) + (Sum (Fr2 | (n + 1))) ) by A4, A5, A25, AFINSQ_2:65;
then ( Sum Fr2 = ((Partial_Sums (seq1 (##) seq2)) . n) + ((seq1 (##) seq2) . (n + 1)) & n in NAT & n + 1 in NAT ) by A6, A11, A4, A27, A2, A26, A12, ORDINAL1:def 12;
hence ( (Partial_Sums (seq1 (##) seq2)) . (n + 1) = Sum Fr2 & dom Fr2 = (n + 1) + 1 & ( for i being Nat st i in (n + 1) + 1 holds
Fr2 . i = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) ) ) by A4, A5, SERIES_1:def 1; :: thesis:

end;

reconsider rr = (seq1 . 0) * (seq2 . 0) as Element of REAL ;
set Fr = 1 --> rr;
reconsider Fr = 1 --> rr as XFinSequence of REAL ;
take Fr ; :: thesis:
A29: dom Fr = 1 ;
A30: Sum (Fr | zz) = 0 ;
A31: 0 in Segm 1 by NAT_1:44;
then A32: Fr . zz = (seq1 . 0) * (seq2 . 0) by FUNCOP_1:7;
A33: (Sum (Fr | zz)) + (Fr . zz) = Sum (Fr | (zz + 1)) by A29, A31, AFINSQ_2:65;
Sum Fr = Sum (Fr | (0 + 1))
.= (Sum (Fr | zz)) + (Fr . zz) by A33
.= Fr . zz by A30
.= (seq1 (##) seq2) . 0 by Th47, A32 ;
hence ( (Partial_Sums (seq1 (##) seq2)) . 0 = Sum Fr & dom Fr = 0 + 1 ) by SERIES_1:def 1; :: thesis:
let i be Nat; :: thesis:
assume A34: i in 0 + 1 ; :: thesis:
i in Segm 1 by A34;
then i < 1 by NAT_1:44;
then A35: i = 0 by NAT_1:14;
then 0 -' i = 0 by XREAL_1:232;
then (Partial_Sums seq2) . (0 -' i) = seq2 . 0 by SERIES_1:def 1;
hence Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i)) by A34, A35, FUNCOP_1:7; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A28, A1);
hence ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ) ) ; :: thesis: