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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[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: S1[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 ;
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 ;
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 ; :: 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 ; :: 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 ; :: thesis: verum
end;
hence |.(s . m).| < R by ; :: thesis: verum
end;
hence S1[n + 1] by A4; :: thesis: verum
end;
A13: S1[ 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 ;
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 S1[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