let rseq1, rseq2 be Real_Sequence; :: thesis: ( ( for k being 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 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
A1: for k being 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
A2: for k being 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

now :: thesis: for k being Element of NAT holds rseq1 . k = rseq2 . k

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

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

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

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

end;

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

hence rseq1 . k = 0 by A1
.= rseq2 . k by A2, A4 ;
:: thesis: verum

end;

end;

end;

hence rseq1 = rseq2 ; :: thesis: verum