let z be Complex; :: thesis: for n being Nat holds 0 <= (|.z.| rExpSeq) . n
let n be Nat; :: thesis: 0 <= (|.z.| rExpSeq) . n
(|.z.| rExpSeq) . n = |.((z ExpSeq) . n).| by Th3;
hence 0 <= (|.z.| rExpSeq) . n by COMPLEX1:46; :: thesis: verum