let seq be Complex_Sequence; :: thesis: for n being Element of NAT holds
( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n )
let n be Element of 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:132; :: thesis: verum