let s be Complex_Sequence; :: thesis: for n being Nat ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) )

let n be Nat; :: thesis: ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) )

defpred S_{1}[ Nat] means ex r being Real st

( 0 < r & ( for m being Nat st m <= $1 holds

|.(s . m).| < r ) );

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A13, A1);

then consider R being Real such that

A14: ( R > 0 & ( for m being Nat st m <= n holds

|.(s . m).| < R ) ) ;

thus ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) ) by A14; :: thesis: verum

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) )

let n be Nat; :: thesis: ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) )

defpred S

( 0 < r & ( for m being Nat st m <= $1 holds

|.(s . m).| < r ) );

A1: for n being Nat st S

S

proof

A13:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

given R1 being Real such that A2: 0 < R1 and

A3: for m being Nat st m <= n holds

|.(s . m).| < R1 ; :: thesis: S_{1}[n + 1]

_{1}[n + 1]
by A4; :: thesis: verum

end;given R1 being Real such that A2: 0 < R1 and

A3: for m being Nat st m <= n holds

|.(s . m).| < R1 ; :: thesis: S

A4: now :: thesis: ( R1 <= |.(s . (n + 1)).| implies ex R being set st

( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) ) )

( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) ) )

assume A5:
R1 <= |.(s . (n + 1)).|
; :: thesis: ex R being set st

( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

take R = |.(s . (n + 1)).| + 1; :: thesis: ( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

0 + 0 < R by COMPLEX1:46, XREAL_1:8;

hence 0 < R ; :: thesis: for m being Nat st m <= n + 1 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= n + 1 implies |.(s . m).| < R )

assume A6: m <= n + 1 ; :: thesis: |.(s . m).| < R

end;( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

take R = |.(s . (n + 1)).| + 1; :: thesis: ( 0 < R & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

0 + 0 < R by COMPLEX1:46, XREAL_1:8;

hence 0 < R ; :: thesis: for m being Nat st m <= n + 1 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= n + 1 implies |.(s . m).| < R )

assume A6: m <= n + 1 ; :: thesis: |.(s . m).| < R

A7: now :: thesis: ( m <= n implies |.(s . m).| < R )

assume
m <= n
; :: thesis: |.(s . m).| < R

then |.(s . m).| < R1 by A3;

then |.(s . m).| < |.(s . (n + 1)).| by A5, XXREAL_0:2;

then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

end;then |.(s . m).| < R1 by A3;

then |.(s . m).| < |.(s . (n + 1)).| by A5, XXREAL_0:2;

then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

now :: thesis: ( m = n + 1 implies |.(s . m).| < R )

hence
|.(s . m).| < R
by A6, A7, NAT_1:8; :: thesis: verumassume
m = n + 1
; :: thesis: |.(s . m).| < R

then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

end;then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

now :: thesis: ( |.(s . (n + 1)).| <= R1 implies ex R being set st

( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) ) )

hence
S( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) ) )

assume A8:
|.(s . (n + 1)).| <= R1
; :: thesis: ex R being set st

( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

take R = R1 + 1; :: thesis: ( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

thus R > 0 by A2; :: thesis: for m being Nat st m <= n + 1 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= n + 1 implies |.(s . m).| < R )

assume A9: m <= n + 1 ; :: thesis: |.(s . m).| < R

end;( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

take R = R1 + 1; :: thesis: ( R > 0 & ( for m being Nat st m <= n + 1 holds

|.(s . m).| < R ) )

thus R > 0 by A2; :: thesis: for m being Nat st m <= n + 1 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= n + 1 implies |.(s . m).| < R )

assume A9: m <= n + 1 ; :: thesis: |.(s . m).| < R

A10: now :: thesis: ( m <= n implies |.(s . m).| < R )

assume
m <= n
; :: thesis: |.(s . m).| < R

then A11: |.(s . m).| < R1 by A3;

R1 + 0 < R by XREAL_1:8;

hence |.(s . m).| < R by A11, XXREAL_0:2; :: thesis: verum

end;then A11: |.(s . m).| < R1 by A3;

R1 + 0 < R by XREAL_1:8;

hence |.(s . m).| < R by A11, XXREAL_0:2; :: thesis: verum

now :: thesis: ( m = n + 1 implies |.(s . m).| < R )

hence
|.(s . m).| < R
by A9, A10, NAT_1:8; :: thesis: verumA12:
R1 + 0 < R
by XREAL_1:8;

assume m = n + 1 ; :: thesis: |.(s . m).| < R

hence |.(s . m).| < R by A8, A12, XXREAL_0:2; :: thesis: verum

end;assume m = n + 1 ; :: thesis: |.(s . m).| < R

hence |.(s . m).| < R by A8, A12, XXREAL_0:2; :: thesis: verum

proof

for n being Nat holds S
take R = |.(s . 0).| + 1; :: thesis: ( 0 < R & ( for m being Nat st m <= 0 holds

|.(s . m).| < R ) )

0 + 0 < |.(s . 0).| + 1 by COMPLEX1:46, XREAL_1:8;

hence 0 < R ; :: thesis: for m being Nat st m <= 0 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= 0 implies |.(s . m).| < R )

assume m <= 0 ; :: thesis: |.(s . m).| < R

then m = 0 ;

then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

end;|.(s . m).| < R ) )

0 + 0 < |.(s . 0).| + 1 by COMPLEX1:46, XREAL_1:8;

hence 0 < R ; :: thesis: for m being Nat st m <= 0 holds

|.(s . m).| < R

let m be Nat; :: thesis: ( m <= 0 implies |.(s . m).| < R )

assume m <= 0 ; :: thesis: |.(s . m).| < R

then m = 0 ;

then |.(s . m).| + 0 < R by XREAL_1:8;

hence |.(s . m).| < R ; :: thesis: verum

then consider R being Real such that

A14: ( R > 0 & ( for m being Nat st m <= n holds

|.(s . m).| < R ) ) ;

thus ex r being Real st

( 0 < r & ( for m being Nat st m <= n holds

|.(s . m).| < r ) ) by A14; :: thesis: verum