let seq1, seq2 be sequence of X; :: thesis: ( ( for k being Nat holds

( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (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 = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( k > n implies seq1 . k = 0. X ) ) and

A2: for k being Nat holds

( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( k > n implies seq2 . k = 0. X ) ) ; :: thesis: seq1 = seq2

( ( k <= n implies seq1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies seq1 . k = 0. X ) ) ) & ( for k being Nat holds

( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (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 = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( k > n implies seq1 . k = 0. X ) ) and

A2: for k being Nat holds

( ( k <= n implies seq2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (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

hence
seq1 = seq2
by FUNCT_2:63; :: thesis: verumlet k be Element of NAT ; :: thesis: seq1 . b_{1} = seq2 . b_{1}

end;