let X be Banach_Algebra; :: thesis: for z being Element of X
for m, n being Nat holds
( |.((Partial_Sums (||.z.|| rExpSeq)) . n).| = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)).| = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) )
let z be Element of X; :: thesis: for m, n being Nat holds
( |.((Partial_Sums (||.z.|| rExpSeq)) . n).| = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)).| = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) )
let m, n be Nat; :: thesis: ( |.((Partial_Sums (||.z.|| rExpSeq)) . n).| = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)).| = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) )
for n being Nat holds 0 <= (||.z.|| rExpSeq) . n by Th27;
hence ( |.((Partial_Sums (||.z.|| rExpSeq)) . n).| = (Partial_Sums (||.z.|| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n)).| = ((Partial_Sums (||.z.|| rExpSeq)) . m) - ((Partial_Sums (||.z.|| rExpSeq)) . n) ) ) by COMSEQ_3:9; :: thesis: verum