let seq1, seq2 be sequence of X; :: thesis: ( ( for k being Nat holds
( ( k <= n implies seq1 . k = (((Coef 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 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 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 n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( k > n implies seq2 . k = 0. X ) ) ; :: thesis: seq1 = seq2

now :: thesis: for k being Element of NAT holds seq1 . k = seq2 . k

let k be Element of NAT ; :: thesis: seq1 . b₁ = seq2 . b₁

per cases ( k <= n or k > n ) ;

suppose A3: k <= n ; :: thesis: seq1 . b₁ = seq2 . b₁

hence seq1 . k = (((Coef n) . k) * (z #N k)) * (w #N (n -' k)) by A1
.= seq2 . k by A2, A3 ;
:: thesis: verum

end;

suppose A4: k > n ; :: thesis: seq1 . b₁ = seq2 . b₁

hence seq1 . k = 0. X by A1
.= seq2 . k by A2, A4 ;
:: thesis: verum

end;

end;

end;

hence seq1 = seq2 by FUNCT_2:63; :: thesis: verum