let seq be Complex_Sequence; :: thesis: ( seq is bounded & sup (rng |.seq.|) = 0 implies for n being Element of NAT holds seq . n = 0c )
assume that
A1: seq is bounded and
A2: sup (rng |.seq.|) = 0 ; :: thesis: for n being Element of NAT holds seq . n = 0c
let n be Element of NAT ; :: thesis: seq . n = 0c
A3: |.seq.| is bounded by A1, Lm9;
0 <= |.(seq . n).| by COMPLEX1:132;
then 0 <= |.seq.| . n by VALUED_1:18;
then |.seq.| . n = 0 by A2, A3, Lm2;
then |.(seq . n).| = 0 by VALUED_1:18;
hence seq . n = 0c by COMPLEX1:131; :: thesis: verum