let z be Element of COMPLEX ; :: thesis: for n being Element of NAT holds 0 <= (|.z.| rExpSeq ) . n
let n be Element of NAT ; :: thesis: 0 <= (|.z.| rExpSeq ) . n
A1: (|.z.| rExpSeq ) . n = |.((z ExpSeq ) . n).| by Th4;
thus 0 <= (|.z.| rExpSeq ) . n by A1, COMPLEX1:132; :: thesis: verum