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₁[ 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[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₁[n + 1]

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

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

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;

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

assume m = n + 1 ; :: thesis: |.(s . m).| < R
then |.(s . m).| + 0 < R by XREAL_1:8;
hence |.(s . m).| < R ; :: thesis: verum

end;

hence |.(s . m).| < R by A6, A7, NAT_1:8; :: thesis: verum

end;

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

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

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;

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

A12: 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;

hence |.(s . m).| < R by A9, A10, NAT_1:8; :: thesis: verum

end;

hence S₁[n + 1] by A4; :: thesis: verum

end;

A13: S₁[ 0 ]

proof

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;

for n being Nat holds S₁[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