let X be Complex_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 S_{1}[ Nat] means (Partial_Sums seq) . $1 = ((Partial_Sums (Shift seq)) . $1) + (seq . $1);

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= (0. X) + (seq . 0) by RLVECT_1:4

.= ((Shift seq) . 0) + (seq . 0) by LOPBAN_4:def 5

.= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by BHSP_4:def 1 ;

then A2: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A2, A1);

hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: verum

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 S

A1: for k being Nat st S

S

proof

(Partial_Sums seq) . 0 =
seq . 0
by BHSP_4:def 1
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: S_{1}[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 LOPBAN_4:def 5

.= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by BHSP_4:def 1 ;

:: thesis: verum

end;assume (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: S

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 LOPBAN_4:def 5

.= ((Partial_Sums (Shift seq)) . (k + 1)) + (seq . (k + 1)) by BHSP_4:def 1 ;

:: thesis: verum

.= (0. X) + (seq . 0) by RLVECT_1:4

.= ((Shift seq) . 0) + (seq . 0) by LOPBAN_4:def 5

.= ((Partial_Sums (Shift seq)) . 0) + (seq . 0) by BHSP_4:def 1 ;

then A2: S

for k being Nat holds S

hence (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k) ; :: thesis: verum