let c be Complex; :: thesis:
let seq be Complex_Sequence; :: thesis:
assume seq is bounded ; :: thesis:
then consider r being Real such that
0 < r and
A1: for n being Nat holds |.(seq . n).| < r by COMSEQ_2:8;
ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1

take r1 = 1; :: thesis:
for n being Nat holds |.((c (#) seq) . n).| < jj

let n be Nat; :: thesis:
(c (#) seq) . n = c * (seq . n) by VALUED_1:6
.= 0 by A2 ;
hence |.((c (#) seq) . n).| < jj by COMPLEX1:44; :: thesis:

end;

hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis:

end;

end;

hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis:

end;

hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis:

end;