let seq3, seq4 be Real_Sequence; :: thesis:
assume that
A6: for k being Nat ex Fr being XFinSequence of REAL 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 ) and
A7: for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = seq4 . k ) ; :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider k = x as Nat ;
consider Fr1 being XFinSequence of REAL such that
A8: dom Fr1 = k + 1 and
A9: for n being Nat st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A10: Sum Fr1 = seq3 . k by A6;
consider Fr2 being XFinSequence of REAL such that
A11: dom Fr2 = k + 1 and
A12: for n being Nat st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) and
A13: Sum Fr2 = seq4 . k by A7;

let n be Nat; :: thesis:
assume A14: n in dom Fr1 ; :: thesis:
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) by A8, A9, A14;
hence Fr1 . n = Fr2 . n by A8, A12, A14; :: thesis:

end;

end;