let seq1, seq2 be Complex_Sequence; :: thesis: for m being Nat st ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
let m be Nat; :: thesis: ( ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m )
defpred S₁[ Nat] means ( $1 <= m implies (Partial_Sums seq1) . $1 = (Partial_Sums seq2) . $1 );
assume A1: for n being Nat st n <= m holds
seq1 . n = seq2 . n ; :: thesis: (Partial_Sums seq1) . m = (Partial_Sums seq2) . m
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
assume A4: k + 1 <= m ; :: thesis: (Partial_Sums seq1) . (k + 1) = (Partial_Sums seq2) . (k + 1)
k < k + 1 by XREAL_1:29;
hence (Partial_Sums seq1) . (k + 1) = ((Partial_Sums seq2) . k) + (seq1 . (k + 1)) by A3, A4, SERIES_1:def 1, XXREAL_0:2
.= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4
.= (Partial_Sums seq2) . (k + 1) by SERIES_1:def 1 ;
:: thesis: verum

end;

A5: S₁[ 0 ]

proof

assume 0 <= m ; :: thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0
thus (Partial_Sums seq1) . 0 = seq1 . 0 by SERIES_1:def 1
.= seq2 . 0 by A1
.= (Partial_Sums seq2) . 0 by SERIES_1:def 1 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A2);
hence (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; :: thesis: verum