let X be Banach_Algebra; :: thesis: for m being Nat
for seq1, seq2 being sequence of X 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 seq1, seq2 being sequence of X st ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) holds
(Partial_Sums seq1) . m = (Partial_Sums seq2) . m
let seq1, seq2 be sequence of X; :: thesis: ( ( for n being Nat st n <= m holds
seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m )
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[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, BHSP_4:def 1, XXREAL_0:2
.= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4
.= (Partial_Sums seq2) . (k + 1) by BHSP_4:def 1 ;
:: thesis: verum
end;
A5: S1[ 0 ]
proof
assume 0 <= m ; :: thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0
thus (Partial_Sums seq1) . 0 = seq1 . 0 by BHSP_4:def 1
.= seq2 . 0 by A1
.= (Partial_Sums seq2) . 0 by BHSP_4:def 1 ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A5, A2);
 hence (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; :: thesis: verum