let s be Complex_Sequence; 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; 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;
( 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
;
S1[n + 1]
hence
S1[
n + 1]
by A4;
verum
end;
A13:
S1[ 0 ]
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; verum