let seq3, seq4 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 ) ) & ( 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 = 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 Element of 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 Element of 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 A8: x in NAT ; :: thesis: seq3 . x = seq4 . x
reconsider k = x as Element of NAT by A8;
consider Fr1 being XFinSequence of such that
A9: dom Fr1 = k + 1 and
A10: for n being Element of NAT st n in k + 1 holds
Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) and
A11: Sum Fr1 = seq3 . k by A6;
consider Fr2 being XFinSequence of such that
A12: dom Fr2 = k + 1 and
A13: for n being Element of NAT st n in k + 1 holds
Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) and
A14: Sum Fr2 = seq4 . k by A7;

now

let n be Element of NAT ; :: thesis: ( n in dom Fr1 implies Fr1 . n = Fr2 . n )
assume A15: n in dom Fr1 ; :: thesis: Fr1 . n = Fr2 . n
( Fr1 . n = (seq1 . n) * (seq2 . (k -' n)) & Fr2 . n = (seq1 . n) * (seq2 . (k -' n)) ) by A9, A10, A13, A15;
hence Fr1 . n = Fr2 . n ; :: thesis: verum

end;

hence seq3 . x = seq4 . x by A9, A11, A12, A14, AFINSQ_1:10; :: thesis: verum

end;

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