let seq3, seq1, seq2 be Real_Sequence; :: thesis: ( ( for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq3 . k ) ) implies for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = seq3 . k ) )
assume A16: for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq3 . k ) ; :: thesis: for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = seq3 . k )
let k be Nat; :: thesis: ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = seq3 . k )
reconsider k' = k as Element of NAT by ORDINAL1:def 13;
defpred S₁[ set , set ] means for i being Element of NAT st i = $1 holds
$2 = (seq2 . i) * (seq1 . (k -' i));
A17: for i being Element of NAT st i in k' + 1 holds
ex z being Element of REAL st S₁[i,z]

proof

let i be Element of NAT ; :: thesis: ( i in k' + 1 implies ex z being Element of REAL st S₁[i,z] )
assume i in k' + 1 ; :: thesis: ex z being Element of REAL st S₁[i,z]
take S = (seq2 . i) * (seq1 . (k -' i)); :: thesis: S₁[i,S]
thus S₁[i,S] ; :: thesis: verum

end;

consider Fr1 being XFinSequence of such that
A18: dom Fr1 = k + 1 and
A19: for n being Element of NAT st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A20: Sum Fr1 = seq3 . k by A16;
consider Fr2 being XFinSequence of such that
A21: dom Fr2 = k' + 1 and
A22: for i being Element of NAT st i in k' + 1 holds
S₁[i,Fr2 . i] from STIRL2_1:sch 6(A17);
take Fr2 ; :: thesis: ( dom Fr2 = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr2 . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr2 = seq3 . k )
thus ( dom Fr2 = k + 1 & ( for n being Element of NAT st n in k + 1 holds
Fr2 . n = (seq2 . n) * (seq1 . (k -' n)) ) ) by A21, A22; :: thesis: Sum Fr2 = seq3 . k

now

let n be Element of NAT ; :: thesis: ( n in len Fr1 implies Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) )
assume A23: n in len Fr1 ; :: thesis: Fr1 . n = Fr2 . ((len Fr1) -' (1 + n))
n < k + 1 by A18, A23, NAT_1:45;
then A25: ( n <= k & n + 1 <= k + 1 ) by NAT_1:13;
then ( n + 1 <= len Fr2 & len Fr2 = dom Fr2 & k - n <= k & k < k + 1 ) by A21, NAT_1:13, XREAL_1:45;
then A26: ( (len Fr2) -' (n + 1) = (k + 1) - (n + 1) & k - n < k + 1 ) by A21, XREAL_1:235, XXREAL_0:2;
then A27: (len Fr2) -' (n + 1) in k + 1 by NAT_1:45;
( k -' n <= (k -' n) + n & k -' n = k - n ) by A25, NAT_1:11, XREAL_1:235;
then ( k -' (k -' n) = k - (k -' n) & k -' n = k - n ) by XREAL_1:235;
then ( Fr2 . ((len Fr2) -' (n + 1)) = (seq2 . (k -' n)) * (seq1 . n) & Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) & len Fr1 = dom Fr1 ) by A18, A19, A22, A23, A26, A27;
hence Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) by A18, A21; :: thesis: verum

end;

hence Sum Fr2 = seq3 . k by A18, A20, A21, Lm9; :: thesis: verum