let seq be Complex_Sequence; :: thesis: ( seq is bounded & upper_bound (rng |.seq.|) = 0 implies for n being Nat holds seq . n = 0c )
assume that
A1: seq is bounded and
A2: upper_bound (rng |.seq.|) = 0 ; :: thesis: for n being Nat holds seq . n = 0c
let n be Nat; :: thesis: seq . n = 0c
0 <= |.(seq . n).| by COMPLEX1:46;
then A3: 0 <= |.seq.| . n by VALUED_1:18;
|.seq.| is bounded by A1, Lm8;
then |.seq.| . n = 0 by A2, A3, Lm2;
then |.(seq . n).| = 0 by VALUED_1:18;
hence seq . n = 0c by COMPLEX1:45; :: thesis: verum