let seq3, seq4 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 ) ) & ( 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 = seq4 . k ) ) implies seq3 = seq4 )
assume that
A6: 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 ) and
A7: 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 = seq4 . k ) ; :: thesis: seq3 = seq4

now

let x be set ; :: thesis: ( x in NAT implies seq3 . x = seq4 . x )
assume x in NAT ; :: thesis: seq3 . x = seq4 . x
then reconsider k = x as Element of NAT ;
consider Fr1 being XFinSequence of 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 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;

now

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

end;

hence seq3 . x = seq4 . x by A8, A10, A11, A13, AFINSQ_1:8; :: thesis: verum

end;

hence seq3 = seq4 by FUNCT_2:12; :: thesis: verum