ex m being Nat st
for n being Nat st m <= n holds
||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n

proof

take 0 ; :: thesis: for n being Nat st 0 <= n holds
||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n
thus for n being Nat st 0 <= n holds
||.((z rExpSeq) . n).|| <= (||.z.|| rExpSeq) . n by Th14; :: thesis: verum

end;

hence z rExpSeq is norm_summable by LOPBAN_3:27, SIN_COS:45; :: thesis: verum