let c be Complex; :: thesis: for seq being Complex_Sequence st seq is bounded holds
c (#) seq is bounded

let seq be Complex_Sequence; :: thesis: ( seq is bounded implies c (#) seq is bounded )
assume seq is bounded ; :: thesis: c (#) seq is bounded
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
proof
now :: thesis: ( ( c = 0c & ex r1 being Element of NAT ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ) or ( c <> 0c & ex r1 being set ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ) )
per cases ( c = 0c or c <> 0c ) ;
case A2: c = 0c ; :: thesis: ex r1 being Element of NAT ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1

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

for n being Nat holds |.((c (#) seq) . n).| < jj
proof
let n be Nat; :: thesis: |.((c (#) seq) . n).| < jj
(c (#) seq) . n = c * (seq . n) by VALUED_1:6
.= 0 by A2 ;
hence |.((c (#) seq) . n).| < jj by COMPLEX1:44; :: thesis: verum
end;
hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum
end;
case A3: c <> 0c ; :: thesis: ex r1 being set ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1

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

for n being Nat holds |.((c (#) seq) . n).| < |.c.| * r
proof
let n be Nat; :: thesis: |.((c (#) seq) . n).| < |.c.| * r
A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1:6
.= |.c.| * |.(seq . n).| by COMPLEX1:65 ;
|.c.| > 0 by ;
hence |.((c (#) seq) . n).| < |.c.| * r by ; :: thesis: verum
end;
hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum
end;
end;
end;
hence ex r1 being Real st
for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum
end;
hence c (#) seq is bounded by COMSEQ_2:def 4; :: thesis: verum