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

proof

reconsider r = (abs (seq . 0 )) + 1 as real number ;
take r ; :: thesis: ( 0 < r & ( for m being Element of NAT st m <= 0 holds
abs (seq . m) < r ) )
0 + 0 < (abs (seq . 0 )) + 1 by COMPLEX1:132, XREAL_1:10;
hence 0 < r ; :: thesis: for m being Element of NAT st m <= 0 holds
abs (seq . m) < r
let m be Element of NAT ; :: thesis: ( m <= 0 implies abs (seq . m) < r )
assume A2: m <= 0 ; :: thesis: abs (seq . m) < r
0 = m by A2, NAT_1:2;
then (abs (seq . m)) + 0 < r by XREAL_1:10;
hence abs (seq . m) < r ; :: thesis: verum

end;

A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
given r1 being real number such that A4: 0 < r1 and
A5: for m being Element of NAT st m <= n holds
abs (seq . m) < r1 ; :: thesis: S₁[n + 1]

A6: now

assume A7: abs (seq . (n + 1)) <= r1 ; :: thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
take r = r1 + 1; :: thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
0 + 0 < r1 + 1 by A4;
hence 0 < r ; :: thesis: for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r
let m be Element of NAT ; :: thesis: ( m <= n + 1 implies abs (seq . m) < r )
assume A8: m <= n + 1 ; :: thesis: abs (seq . m) < r

A9: now

assume m <= n ; :: thesis: abs (seq . m) < r
then A10: abs (seq . m) < r1 by A5;
r1 + 0 < r by XREAL_1:10;
hence abs (seq . m) < r by A10, XXREAL_0:2; :: thesis: verum

end;

now

assume A11: m = n + 1 ; :: thesis: abs (seq . m) < r
r1 + 0 < r by XREAL_1:10;
hence abs (seq . m) < r by A7, A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

now

assume A12: r1 <= abs (seq . (n + 1)) ; :: thesis: ex r being Element of REAL st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
take r = (abs (seq . (n + 1))) + 1; :: thesis: ( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) )
0 + 0 < r by COMPLEX1:132, XREAL_1:10;
hence 0 < r ; :: thesis: for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r
let m be Element of NAT ; :: thesis: ( m <= n + 1 implies abs (seq . m) < r )
assume A13: m <= n + 1 ; :: thesis: abs (seq . m) < r

A14: now

assume m <= n ; :: thesis: abs (seq . m) < r
then abs (seq . m) < r1 by A5;
then abs (seq . m) < abs (seq . (n + 1)) by A12, XXREAL_0:2;
then (abs (seq . m)) + 0 < r by XREAL_1:10;
hence abs (seq . m) < r ; :: thesis: verum

end;

now

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

end;

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

end;

hence ex r being real number st
( 0 < r & ( for m being Element of NAT st m <= n + 1 holds
abs (seq . m) < r ) ) by A6; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A3); :: thesis: verum