let seq1, seq2 be Real_Sequence; :: thesis:
let n be Element of NAT ; :: thesis:
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 Element of NAT st i in $1 + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . ($1 -' i)) ) );
A1: S₁[ 0 ]

proof

set Fr = 1 --> ((seq1 . 0 ) * (seq2 . 0 ));
dom (1 --> ((seq1 . 0 ) * (seq2 . 0 ))) = 1 by FUNCOP_1:19;
then reconsider Fr = 1 --> ((seq1 . 0 ) * (seq2 . 0 )) as XFinSequence by AFINSQ_1:7;
reconsider Fr = Fr as XFinSequence of ;
take Fr ; :: thesis:
( dom Fr = 1 & 0 in 1 & Fr | 0 = {} ) by FUNCOP_1:19, NAT_1:45;
then ( (Sum (Fr | 0 )) + (Fr . 0 ) = Sum (Fr | (0 + 1)) & Fr . 0 = (seq1 . 0 ) * (seq2 . 0 ) & dom (Fr | 0 ) = 0 & Fr | 1 = Fr ) by Lm8, FUNCOP_1:13, RELAT_1:98;
then Sum Fr = 0 + ((seq1 . 0 ) * (seq2 . 0 )) by Lm6;
then Sum Fr = (seq1 (##) seq2) . 0 by Th52;
hence ( (Partial_Sums (seq1 (##) seq2)) . 0 = Sum Fr & dom Fr = 0 + 1 ) by FUNCOP_1:19, SERIES_1:def 1; :: thesis:
let i be Element of NAT ; :: thesis:
assume A2: i in 0 + 1 ; :: thesis:
i < 1 by A2, NAT_1:45;
then A3: i = 0 by NAT_1:14;
then ( 0 -' i = 0 & dom Fr = 1 ) by FUNCOP_1:19, XREAL_1:234;
then ( (Partial_Sums seq2) . (0 -' i) = seq2 . 0 & Fr . 0 = (seq1 . 0 ) * (seq2 . 0 ) ) by A2, A3, FUNCOP_1:13, SERIES_1:def 1;
hence Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (0 -' i)) by A3; :: thesis:

end;

A4: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis:
set n1 = n + 1;
assume S₁[n] ; :: thesis:
then consider Fr being XFinSequence of such that
A5: (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr and
A6: dom Fr = n + 1 and
A7: for i being Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ;
consider Fr1 being XFinSequence of such that
A8: dom Fr1 = (n + 1) + 1 and
A9: for i being Element of NAT st i in (n + 1) + 1 holds
Fr1 . i = (seq1 . i) * (seq2 . ((n + 1) -' i)) and
A10: Sum Fr1 = (seq1 (##) seq2) . (n + 1) by Def5;
defpred S₂[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i));
A11: for i being Element of NAT st i in (n + 1) + 1 holds
ex x being Element of REAL st S₂[i,x]

proof

let i be Element of NAT ; :: thesis:
assume i in (n + 1) + 1 ; :: thesis:
take (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) ; :: thesis:
thus S₂[i,(seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i))] ; :: thesis:

end;

consider Fr2 being XFinSequence of such that
A12: dom Fr2 = (n + 1) + 1 and
A13: for i being Element of NAT st i in (n + 1) + 1 holds
S₂[i,Fr2 . i] from STIRL2_1:sch 6(A11);
take Fr2 ; :: thesis:
A14: for i being Element of NAT st i in dom (Fr2 | (n + 1)) holds
(Fr2 | (n + 1)) . i = addreal . (Fr . i),((Fr1 | (n + 1)) . i)

proof

let i be Element of NAT ; :: thesis:
assume A15: i in dom (Fr2 | (n + 1)) ; :: thesis:
i in (dom Fr2) /\ (n + 1) by A15, RELAT_1:90;
then A16: ( i in (n + 1) + 1 & i in n + 1 & i in dom (Fr1 | (n + 1)) ) by A8, A12, RELAT_1:90, XBOOLE_0:def 4;
then A17: ( Fr1 . i = (seq1 . i) * (seq2 . ((n + 1) -' i)) & Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) & Fr2 . i = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) ) by A7, A9, A13;
( i < (n + 1) + 1 & i < n + 1 ) by A16, NAT_1:45;
then ( i <= n + 1 & i <= n ) by NAT_1:13;
then ( (n + 1) -' i = (n + 1) - i & n -' i = n - i ) by XREAL_1:235;
then (n -' i) + 1 = (n + 1) -' i ;
then (Partial_Sums seq2) . ((n + 1) -' i) = ((Partial_Sums seq2) . (n -' i)) + (seq2 . ((n + 1) -' i)) by SERIES_1:def 1;
then ( Fr2 . i = (Fr . i) + (Fr1 . i) & Fr1 . i = (Fr1 | (n + 1)) . i & Fr2 . i = (Fr2 | (n + 1)) . i ) by A15, A16, A17, FUNCT_1:70;
hence (Fr2 | (n + 1)) . i = addreal . (Fr . i),((Fr1 | (n + 1)) . i) by BINOP_2:def 9; :: thesis:

end;

set A = addreal ;
n + 1 <= (n + 1) + 1 by NAT_1:11;
then n + 1 c= (n + 1) + 1 by NAT_1:40;
then ( dom (Fr2 | (n + 1)) = n + 1 & dom (Fr1 | (n + 1)) = n + 1 & dom Fr = len Fr ) by A8, A12, RELAT_1:91;
then ( len (Fr2 | (n + 1)) = len Fr & len (Fr1 | (n + 1)) = len Fr ) by A6;
then addreal "**" (Fr2 | (n + 1)) = addreal "**" (Fr ^ (Fr1 | (n + 1))) by A14, CARD_FIN:62;
then Sum (Fr2 | (n + 1)) = addreal . (Sum Fr),(Sum (Fr1 | (n + 1))) by STIRL2_1:47;
then A18: Sum (Fr2 | (n + 1)) = (Sum Fr) + (Sum (Fr1 | (n + 1))) by BINOP_2:def 9;
n + 1 < (n + 1) + 1 by NAT_1:13;
then A19: n + 1 in (n + 1) + 1 by NAT_1:45;
then A20: ( Fr1 . (n + 1) = (seq1 . (n + 1)) * (seq2 . ((n + 1) -' (n + 1))) & (n + 1) -' (n + 1) = 0 & (Partial_Sums seq2) . 0 = seq2 . 0 & Fr2 . (n + 1) = (seq1 . (n + 1)) * ((Partial_Sums seq2) . ((n + 1) -' (n + 1))) ) by A9, A13, SERIES_1:def 1, XREAL_1:234;
( Sum (Fr2 | ((n + 1) + 1)) = (Fr2 . (n + 1)) + (Sum (Fr2 | (n + 1))) & Sum (Fr1 | ((n + 1) + 1)) = (Fr1 . (n + 1)) + (Sum (Fr1 | (n + 1))) & Fr2 | ((n + 1) + 1) = Fr2 & Fr1 | ((n + 1) + 1) = Fr1 ) by A8, A12, A19, Lm8, RELAT_1:98;
then Sum Fr2 = ((Partial_Sums (seq1 (##) seq2)) . n) + ((seq1 (##) seq2) . (n + 1)) by A5, A10, A18, A20;
hence ( (Partial_Sums (seq1 (##) seq2)) . (n + 1) = Sum Fr2 & dom Fr2 = (n + 1) + 1 & ( for i being Element of NAT st i in (n + 1) + 1 holds
Fr2 . i = (seq1 . i) * ((Partial_Sums seq2) . ((n + 1) -' i)) ) ) by A12, A13, SERIES_1:def 1; :: thesis:

end;

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