let X be Complex_Banach_Algebra; :: thesis: for k being Nat

for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

let k be Nat; :: thesis: for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

let seq be sequence of X; :: thesis: ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

defpred S_{1}[ Nat] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1;

.= ||.(seq . 0).|| by NORMSP_0:def 4 ;

then A4: S_{1}[ 0 ]
by BHSP_4:def 1;

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

hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; :: thesis: verum

for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

let k be Nat; :: thesis: for seq being sequence of X holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

let seq be sequence of X; :: thesis: ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

defpred S

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

S_{1}[k + 1]

(Partial_Sums ||.seq.||) . 0 =
||.seq.|| . 0
by SERIES_1:def 1
S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then A2: ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by XREAL_1:6;

A3: ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| by CLVECT_1:def 13;

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

then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by A3, A2, XXREAL_0:2;

then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by NORMSP_0:def 4;

hence S_{1}[k + 1]
by SERIES_1:def 1; :: thesis: verum

end;assume S

then A2: ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by XREAL_1:6;

A3: ||.(((Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ||.((Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).|| by CLVECT_1:def 13;

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

then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).|| by A3, A2, XXREAL_0:2;

then ||.((Partial_Sums seq) . (k + 1)).|| <= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by NORMSP_0:def 4;

hence S

.= ||.(seq . 0).|| by NORMSP_0:def 4 ;

then A4: S

for k being Nat holds S

hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; :: thesis: verum