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

proof

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

end;

||.z.|| rExpSeq is summable by SIN_COS:49;
hence z rExpSeq is norm_summable by A1, LOPBAN_3:32; :: thesis: verum