let seq be Real_Sequence; :: thesis: for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )
defpred S₁[ Nat] means ex r1 being Real st
( 0 < r1 & ( for m being Nat st m <= $1 holds
|.(seq . m).| < r1 ) );
A1: S₁[ 0 ]

proof

reconsider r = |.(seq . 0).| + 1 as Real ;
take r ; :: thesis: ( 0 < r & ( for m being Nat st m <= 0 holds
|.(seq . m).| < r ) )
0 + 0 < |.(seq . 0).| + 1 by COMPLEX1:46, XREAL_1:8;
hence 0 < r ; :: thesis: for m being Nat st m <= 0 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= 0 implies |.(seq . m).| < r )
assume m <= 0 ; :: thesis: |.(seq . m).| < r
then 0 = m ;
then |.(seq . m).| + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum

end;

A2: 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 A3: 0 < r1 and
A4: for m being Nat st m <= n holds
|.(seq . m).| < r1 ; :: thesis: S₁[n + 1]

A5: now :: thesis: ( |.(seq . (n + 1)).| <= r1 implies ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) ) )

assume A6: |.(seq . (n + 1)).| <= r1 ; :: thesis: ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = r1 + 1; :: thesis: ( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
thus 0 < r by A3; :: thesis: for m being Nat st m <= n + 1 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A7: m <= n + 1 ; :: thesis: |.(seq . m).| < r

A8: now :: thesis: ( m <= n implies |.(seq . m).| < r )

assume m <= n ; :: thesis: |.(seq . m).| < r
then A9: |.(seq . m).| < r1 by A4;
r1 + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r by A9, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: ( m = n + 1 implies |.(seq . m).| < r )

assume A10: m = n + 1 ; :: thesis: |.(seq . m).| < r
r1 + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r by A6, A10, XXREAL_0:2; :: thesis: verum

end;

hence |.(seq . m).| < r by A7, A8, NAT_1:8; :: thesis: verum

end;

now :: thesis: ( r1 <= |.(seq . (n + 1)).| implies ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) ) )

assume A11: r1 <= |.(seq . (n + 1)).| ; :: thesis: ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = |.(seq . (n + 1)).| + 1; :: thesis: ( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
0 + 0 < r by COMPLEX1:46, XREAL_1:8;
hence 0 < r ; :: thesis: for m being Nat st m <= n + 1 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A12: m <= n + 1 ; :: thesis: |.(seq . m).| < r

A13: now :: thesis: ( m <= n implies |.(seq . m).| < r )

assume m <= n ; :: thesis: |.(seq . m).| < r
then |.(seq . m).| < r1 by A4;
then |.(seq . m).| < |.(seq . (n + 1)).| by A11, XXREAL_0:2;
then |.(seq . m).| + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum

end;

now :: thesis: ( m = n + 1 implies |.(seq . m).| < r )

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

end;

hence |.(seq . m).| < r by A12, A13, NAT_1:8; :: thesis: verum

end;

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

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2); :: thesis: verum