let seq be Complex_Sequence; :: thesis: for n being Nat holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
let n be Nat; :: thesis: ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
|.(seq . n).| = |.seq.| . n by VALUED_1:18;
hence ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) by COMPLEX1:46; :: thesis: verum