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

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