ex m being Nat st

for n being Nat st m <= n holds

||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

for n being Nat st m <= n holds

||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

proof

hence
z ExpSeq is norm_summable
by CLOPBAN3:27, SIN_COS:45; :: thesis: verum
take
0
; :: thesis: for n being Nat st 0 <= n holds

||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

thus for n being Nat st 0 <= n holds

||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th13; :: thesis: verum

end;||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

thus for n being Nat st 0 <= n holds

||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th13; :: thesis: verum