let seq1, seq2 be Complex_Sequence; :: thesis: ( ( for k being Element of NAT holds
( ( k <= n implies seq1 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( n < k implies seq1 . k = 0 ) ) ) & ( for k being Element of NAT holds
( ( k <= n implies seq2 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( n < k implies seq2 . k = 0 ) ) ) implies seq1 = seq2 )
assume that
A2: for k being Element of NAT holds
( ( k <= n implies seq1 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( k > n implies seq1 . k = 0 ) ) and
A3: for k being Element of NAT holds
( ( k <= n implies seq2 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) ) & ( k > n implies seq2 . k = 0 ) ) ; :: thesis: seq1 = seq2

A4: now

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

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

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

thus seq1 . k = ((z ExpSeq ) . k) * ((Partial_Sums (w ExpSeq )) . (n -' k)) by A2, A5
.= seq2 . k by A3, A5 ; :: thesis: verum

end;

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

thus seq1 . k = 0c by A2, A6
.= seq2 . k by A3, A6 ; :: thesis: verum

end;

end;

end;

thus seq1 = seq2 by A4, FUNCT_2:113; :: thesis: verum