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

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

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum

end;

hence
c (#) seq is bounded
by COMSEQ_2:def 4; :: thesis: verumnow :: 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 ) )end;

hence
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 )
;

end;

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

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

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum

end;for n being Nat holds |.((c (#) seq) . n).| < r1

for n being Nat holds |.((c (#) seq) . n).| < jj

proof

hence
ex r1 being Real st
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;(c (#) seq) . n = c * (seq . n) by VALUED_1:6

.= 0 by A2 ;

hence |.((c (#) seq) . n).| < jj by COMPLEX1:44; :: thesis: verum

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum

case A3:
c <> 0c
; :: thesis: ex r1 being set ex r1 being Real st

for n being Nat holds |.((c (#) seq) . n).| < r1

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

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum

end;for n being Nat holds |.((c (#) seq) . n).| < r1

for n being Nat holds |.((c (#) seq) . n).| < |.c.| * r

proof

hence
ex r1 being Real st
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 A3, COMPLEX1:47;

hence |.((c (#) seq) . n).| < |.c.| * r by A1, A4, XREAL_1:68; :: thesis: verum

end;A4: |.((c (#) seq) . n).| = |.(c * (seq . n)).| by VALUED_1:6

.= |.c.| * |.(seq . n).| by COMPLEX1:65 ;

|.c.| > 0 by A3, COMPLEX1:47;

hence |.((c (#) seq) . n).| < |.c.| * r by A1, A4, XREAL_1:68; :: thesis: verum

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum

for n being Nat holds |.((c (#) seq) . n).| < r1 ; :: thesis: verum