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 Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8;
ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1

proof

now

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 Element of NAT holds |.((c (#) seq) . n).| < r1

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

proof

let n be Element of NAT ; :: thesis: |.((c (#) seq) . n).| < 1
(c (#) seq) . n = c * (seq . n) by VALUED_1:6
.= 0 by A2 ;
hence |.((c (#) seq) . n).| < 1 by COMPLEX1:130; :: thesis: verum

end;

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

end;

case A3: c <> 0c ; :: thesis: ex r1 being Element of REAL ex r1 being Real st
for n being Element of NAT holds |.((c (#) seq) . n).| < r1

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

proof

let n be Element of NAT ; :: thesis: |.((c (#) seq) . n).| < |.c.| * r
A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1:6
.= |.c.| * |.(seq . n).| by COMPLEX1:151 ;
|.c.| > 0 by A3, COMPLEX1:133;
hence |.((c (#) seq) . n).| < |.c.| * r by A1, A4, XREAL_1:70; :: thesis: verum

end;

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

end;

end;

end;

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

end;

hence c (#) seq is bounded by COMSEQ_2:def 3; :: thesis: verum