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 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 Nat st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = seq3 . k ) )
assume A15: for k being Nat ex Fr being XFinSequence of st
( dom Fr = k + 1 & ( for n being 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 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 Nat st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = seq3 . k )
consider Fr1 being XFinSequence of such that
A16: dom Fr1 = k + 1 and
A17: for n being Nat st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A18: Sum Fr1 = seq3 . k by A15;
defpred S₁[ set , set ] means for i being Nat st i = $1 holds
$2 = (seq2 . i) * (seq1 . (k -' i));
reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
A19: for i being Nat st i in k9 + 1 holds
ex z being Element of REAL st S₁[i,z]

proof

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

end;

consider Fr2 being XFinSequence of such that
A20: dom Fr2 = k9 + 1 and
A21: for i being Nat st i in k9 + 1 holds
S₁[i,Fr2 . i] from STIRL2_1:sch 5(A19);
take Fr2 ; :: thesis: ( dom Fr2 = k + 1 & ( for n being 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 Nat st n in k + 1 holds
Fr2 . n = (seq2 . n) * (seq1 . (k -' n)) ) ) by A20, A21; :: thesis: Sum Fr2 = seq3 . k

now

let n be Nat; :: thesis: ( n in len Fr1 implies Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) )
assume A22: n in len Fr1 ; :: thesis: Fr1 . n = Fr2 . ((len Fr1) -' (1 + n))
A23: n < k + 1 by A16, A22, NAT_1:44;
then n <= k by NAT_1:13;
then A24: k -' n = k - n by XREAL_1:233;
k -' n <= (k -' n) + n by NAT_1:11;
then A25: k -' (k -' n) = k - (k -' n) by A24, XREAL_1:233;
n + 1 <= len Fr2 by A20, A23, NAT_1:13;
then A26: (len Fr2) -' (n + 1) = (k + 1) - (n + 1) by A20, XREAL_1:233;
( k - n <= k & k < k + 1 ) by NAT_1:13, XREAL_1:43;
then k - n < k + 1 by XXREAL_0:2;
then (len Fr2) -' (n + 1) in k + 1 by A26, NAT_1:44;
then Fr2 . ((len Fr2) -' (n + 1)) = (seq2 . (k -' n)) * (seq1 . n) by A21, A26, A24, A25;
hence Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) by A16, A17, A20, A22; :: thesis: verum

end;

hence Sum Fr2 = seq3 . k by A16, A18, A20, Lm5; :: thesis: verum