let seq1, seq2 be Complex_Sequence; ( ( for k being Nat holds
( ( k <= n implies seq1 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies seq1 . k = 0 ) ) ) & ( for k being Nat holds
( ( k <= n implies seq2 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies seq2 . k = 0 ) ) ) implies seq1 = seq2 )
assume that
A1:
for k being Nat holds
( ( k <= n implies seq1 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( k > n implies seq1 . k = 0 ) )
and
A2:
for k being Nat holds
( ( k <= n implies seq2 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( k > n implies seq2 . k = 0 ) )
; seq1 = seq2
hence
seq1 = seq2
; verum