let seq be Real_Sequence; for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )
defpred S1[ Nat] means ex r1 being Real st
( 0 < r1 & ( for m being Nat st m <= $1 holds
|.(seq . m).| < r1 ) );
A1:
S1[ 0 ]
A2:
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 A3:
0 < r1
and A4:
for
m being
Nat st
m <= n holds
|.(seq . m).| < r1
;
S1[n + 1]
hence
S1[
n + 1]
by A5;
verum
end;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2); verum