let X be 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₁[ Nat] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1;

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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 NORMSP_1:def 1;
||.((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₁[k + 1] by SERIES_1:def 1; :: thesis: verum

end;

(Partial_Sums ||.seq.||) . 0 = ||.seq.|| . 0 by SERIES_1:def 1
.= ||.(seq . 0).|| by NORMSP_0:def 4 ;
then A4: S₁[ 0 ] by BHSP_4:def 1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A1);
hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; :: thesis: verum