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 S1[ Nat] means ||.((Partial_Sums seq) . $1).|| <= (Partial_Sums ||.seq.||) . $1;
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[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 S1[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: S1[ 0 ] by BHSP_4:def 1;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A1);
 hence ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k ; :: thesis: verum