for r being Real st r > 0 holds
ex n0 being Nat st
for n being Nat st n0 <= n holds
|.((Wallis_Seq . n) - (1 / PI)).| < r

proof

let r be Real; :: thesis: ( r > 0 implies ex n0 being Nat st
for n being Nat st n0 <= n holds
|.((Wallis_Seq . n) - (1 / PI)).| < r )
assume r > 0 ; :: thesis: ex n0 being Nat st
for n being Nat st n0 <= n holds
|.((Wallis_Seq . n) - (1 / PI)).| < r
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((w_seq . m) - (1 / PI)).| < r by SEQ_2:def 7, Lm10;
ex n0 being Nat st
for m being Nat st n0 <= m holds
|.((Wallis_Seq . m) - (1 / PI)).| < r

proof

take n1 ; :: thesis: for m being Nat st n1 <= m holds
|.((Wallis_Seq . m) - (1 / PI)).| < r
let m be Nat; :: thesis: ( n1 <= m implies |.((Wallis_Seq . m) - (1 / PI)).| < r )
assume n1 <= m ; :: thesis: |.((Wallis_Seq . m) - (1 / PI)).| < r
then A4: |.((w_seq . m) - (1 / PI)).| < r by A2;
A5: w_seq . m = 1 / ((1 + (1 / (2 * (m + 1)))) * PI) by Def8;
A6: Wallis_Seq . m = (((Product (odd-seq (m + 1))) |^ 2) / ((Product (even-seq (m + 1))) |^ 2)) * (m + 1) by Def7;
then A7: (1 / PI) - (Wallis_Seq . m) >= 0 by Th47, XREAL_1:48;
A8: (1 / PI) - (w_seq . m) > 0 by Lm9, A5;
A9: |.((Wallis_Seq . m) - (1 / PI)).| = |.((1 / PI) - (Wallis_Seq . m)).| by COMPLEX1:60
.= (1 / PI) - (Wallis_Seq . m) by A7, ABSVALUE:def 1 ;
|.((w_seq . m) - (1 / PI)).| = |.((1 / PI) - (w_seq . m)).| by COMPLEX1:60
.= (1 / PI) - (w_seq . m) by A8, ABSVALUE:def 1 ;
then |.((Wallis_Seq . m) - (1 / PI)).| <= |.((w_seq . m) - (1 / PI)).| by A9, XREAL_1:10, A5, A6, Th45;
hence |.((Wallis_Seq . m) - (1 / PI)).| < r by A4, XXREAL_0:2; :: thesis: verum

end;

hence ex n0 being Nat st
for n being Nat st n0 <= n holds
|.((Wallis_Seq . n) - (1 / PI)).| < r ; :: thesis: verum

end;

then consider a being Real such that
A11: a = 1 / PI and
A12: for r being Real st r > 0 holds
ex n0 being Nat st
for n being Nat st n0 <= n holds
|.((Wallis_Seq . n) - a).| < r ;
Wallis_Seq is convergent by A12;
hence ( lim Wallis_Seq = 1 / PI & Wallis_Seq is convergent ) by A11, A12, SEQ_2:def 7; :: thesis: verum