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:46, XREAL_1:8;
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 m <= 0 ; :: thesis: abs (seq . m) < r
then 0 = m by NAT_1:2;
then (abs (seq . m)) + 0 < r by XREAL_1:8;
hence abs (seq . m) < r ; :: thesis: verum

end;

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

A5: now

assume A6: 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 ) )
thus 0 < r by A3; :: 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 A7: m <= n + 1 ; :: thesis: abs (seq . m) < r

A8: now

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

end;

now

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

end;

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

end;

now

assume A11: 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:46, XREAL_1:8;
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 A12: m <= n + 1 ; :: thesis: abs (seq . m) < r

A13: now

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

end;

hence abs (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 Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2); :: thesis: verum