ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

proof

take 0 ; :: thesis: for n being Element of NAT st 0 <= n holds
||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n
thus for n being Element of NAT st 0 <= n holds
||.((z ExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th13; :: thesis: verum

end;

hence z ExpSeq is norm_summable by CLOPBAN3:31, SIN_COS:49; :: thesis: verum