let X be Banach_Algebra; :: thesis: for k being Nat
for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
let k be Nat; :: thesis: for seq being sequence of X holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
let seq be sequence of X; :: thesis: (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
defpred S1[ Nat] means (Partial_Sums seq) . $1 = ((Partial_Sums (Shift seq)) . $1) + (seq . $1);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: S1[k + 1]
hence (Partial_Sums seq) . (k + 1) = (((Partial_Sums (Shift seq)) . k) + (seq . k)) + (seq . (k + 1)) by BHSP_4:def 1
.= (((Partial_Sums (Shift seq)) . k) + ((Shift seq) . (k + 1))) + (seq . (k + 1)) by Def5
.= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by BHSP_4:def 1 ;
:: thesis: verum
end;
(Partial_Sums seq) . 0 = seq . 0 by BHSP_4:def 1
.= (0. X) + (seq . 0) by RLVECT_1:4
.= ((Shift seq) . 0) + (seq . 0) by Def5
.= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by BHSP_4:def 1 ;
then A2: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A1);
 hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: verum