let rseq1, rseq2 be Real_Sequence; :: thesis: ( ( for k being Element of NAT holds
( ( k <= n implies rseq1 . k = ((a rExpSeq ) . k) * (((Partial_Sums (b rExpSeq )) . n) - ((Partial_Sums (b rExpSeq )) . (n -' k))) ) & ( n < k implies rseq1 . k = 0 ) ) ) & ( for k being Element of NAT holds
( ( k <= n implies rseq2 . k = ((a rExpSeq ) . k) * (((Partial_Sums (b rExpSeq )) . n) - ((Partial_Sums (b rExpSeq )) . (n -' k))) ) & ( n < k implies rseq2 . k = 0 ) ) ) implies rseq1 = rseq2 )
assume that
A2: for k being Element of NAT holds
( ( k <= n implies rseq1 . k = ((a rExpSeq ) . k) * (((Partial_Sums (b rExpSeq )) . n) - ((Partial_Sums (b rExpSeq )) . (n -' k))) ) & ( k > n implies rseq1 . k = 0 ) ) and
A3: for k being Element of NAT holds
( ( k <= n implies rseq2 . k = ((a rExpSeq ) . k) * (((Partial_Sums (b rExpSeq )) . n) - ((Partial_Sums (b rExpSeq )) . (n -' k))) ) & ( k > n implies rseq2 . k = 0 ) ) ; :: thesis: rseq1 = rseq2

A4: now

let k be Element of NAT ; :: thesis: rseq1 . b₁ = rseq2 . b₁

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

suppose A5: k <= n ; :: thesis: rseq1 . b₁ = rseq2 . b₁

thus rseq1 . k = ((a rExpSeq ) . k) * (((Partial_Sums (b rExpSeq )) . n) - ((Partial_Sums (b rExpSeq )) . (n -' k))) by A2, A5
.= rseq2 . k by A3, A5 ; :: thesis: verum

end;

suppose A6: k > n ; :: thesis: rseq1 . b₁ = rseq2 . b₁

thus rseq1 . k = 0 by A2, A6
.= rseq2 . k by A3, A6 ; :: thesis: verum

end;

end;

end;

thus rseq1 = rseq2 by A4, FUNCT_2:113; :: thesis: verum