let seq1, seq2 be Real_Sequence; :: thesis: for n being Nat ex Fr being XFinSequence of 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)) ) )
let n be Nat; :: thesis: ex Fr being XFinSequence of 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)) ) )
set S = seq1 (##) seq2;
set P = Partial_Sums seq2;
defpred S₁[ Nat] means ex Fr being XFinSequence of 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]

proof

set A = addreal ;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
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:234;
A3: for i being Nat st i in (n + 1) + 1 holds
ex x being Element of REAL st S₂[i,x]

proof

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

end;

consider Fr2 being XFinSequence of such that
A4: dom Fr2 = (n + 1) + 1 and
A5: for i being Nat st i in (n + 1) + 1 holds
S₂[i,Fr2 . i] from STIRL2_1:sch 5(A3);
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider Fr being XFinSequence of 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 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 Def5;
A12: Fr1 | ((n + 1) + 1) = Fr1 by A9, RELAT_1:98;
A13: for i being Nat st i in dom (Fr2 | (n + 1)) holds
(Fr2 | (n + 1)) . i = addreal . ((Fr . i),((Fr1 | (n + 1)) . i))

proof

let i be Nat; :: thesis: ( i in dom (Fr2 | (n + 1)) implies (Fr2 | (n + 1)) . i = addreal . ((Fr . i),((Fr1 | (n + 1)) . i)) )
assume A14: i in dom (Fr2 | (n + 1)) ; :: thesis: (Fr2 | (n + 1)) . i = addreal . ((Fr . i),((Fr1 | (n + 1)) . i))
A15: i in (dom Fr2) /\ (n + 1) by A14, RELAT_1:90;
then i in dom (Fr1 | (n + 1)) by A9, A4, RELAT_1:90;
then A16: Fr1 . i = (Fr1 | (n + 1)) . i by FUNCT_1:70;
A17: i in n + 1 by A15, XBOOLE_0:def 4;
then A18: i < n + 1 by NAT_1:45;
then i <= n by NAT_1:13;
then A19: n -' i = n - i by XREAL_1:235;
( 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:70;
(n + 1) -' i = (n + 1) - i by A18, XREAL_1:235;
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: verum

end;

n + 1 <= (n + 1) + 1 by NAT_1:11;
then A23: n + 1 c= (n + 1) + 1 by NAT_1:40;
then A24: len (Fr1 | (n + 1)) = len Fr by A7, A9, RELAT_1:91;
n + 1 < (n + 1) + 1 by NAT_1:13;
then A25: n + 1 in (n + 1) + 1 by NAT_1:45;
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:77;
len (Fr2 | (n + 1)) = len Fr by A7, A4, A23, RELAT_1:91;
then addreal "**" (Fr2 | (n + 1)) = addreal "**" (Fr ^ (Fr1 | (n + 1))) by A13, A24, AFINSQ_2:58
.= Sum (Fr ^ (Fr1 | (n + 1))) by AFINSQ_2:60
.= (Sum Fr) + (Sum (Fr1 | (n + 1))) by AFINSQ_2:67 ;
then A27: Sum (Fr2 | (n + 1)) = (Sum Fr) + (Sum (Fr1 | (n + 1))) by AFINSQ_2:60;
take Fr2 ; :: thesis: ( (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)) ) )
( 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:77;
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, RELAT_1:98, ORDINAL1:def 13;
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: verum

end;

A28: S₁[ 0 ]

proof

set Fr = 1 --> ((seq1 . 0) * (seq2 . 0));
reconsider Fr = 1 --> ((seq1 . 0) * (seq2 . 0)) as XFinSequence of ;
take Fr ; :: thesis: ( (Partial_Sums (seq1 (##) seq2)) . 0 = Sum Fr & dom Fr = 0 + 1 & ( for i being Nat st i in 0 + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i)) ) )
A29: dom Fr = 1 by FUNCOP_1:19;
then A30: ( dom (Fr | 0) = 0 & Fr | 1 = Fr ) by RELAT_1:98;
A31: 0 in 1 by NAT_1:45;
then A32: Fr . 0 = (seq1 . 0) * (seq2 . 0) by FUNCOP_1:13;
(Sum (Fr | 0)) + (Fr . 0) = Sum (Fr | (0 + 1)) by A29, A31, AFINSQ_2:77;
then Sum Fr = (seq1 (##) seq2) . 0 by Th52, A32, A30;
hence ( (Partial_Sums (seq1 (##) seq2)) . 0 = Sum Fr & dom Fr = 0 + 1 ) by FUNCOP_1:19, SERIES_1:def 1; :: thesis: for i being Nat st i in 0 + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i))
let i be Nat; :: thesis: ( i in 0 + 1 implies Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i)) )
assume A33: i in 0 + 1 ; :: thesis: Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i))
i < 1 by A33, NAT_1:45;
then A34: i = 0 by NAT_1:14;
then 0 -' i = 0 by XREAL_1:234;
then (Partial_Sums seq2) . (0 -' i) = seq2 . 0 by SERIES_1:def 1;
hence Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i)) by A33, A34, FUNCOP_1:13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A28, A1);
hence ex Fr being XFinSequence of 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: verum