let seq1, seq2 be sequence of X; ( ( for k being Nat holds
( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Nat holds
( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies seq2 . k = 0. X ) ) ) implies seq1 = seq2 )
assume that
A1:
for k being Nat holds
( ( k <= n implies seq1 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq1 . k = 0. X ) )
and
A2:
for k being Nat holds
( ( k <= n implies seq2 . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) )
; seq1 = seq2
hence
seq1 = seq2
by FUNCT_2:63; verum