A1: for k being Nat holds Wallis_Seq . k > 0

proof

let k be Nat; :: thesis: Wallis_Seq . k > 0
Wallis_Seq . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1) by Def7;
hence Wallis_Seq . k > 0 ; :: thesis: verum

end;

for r being Real st r in rng Wallis_Seq holds
0 < r

proof

let r be Real; :: thesis: ( r in rng Wallis_Seq implies 0 < r )
assume r in rng Wallis_Seq ; :: thesis: 0 < r
then ex x being object st
( x in dom Wallis_Seq & r = Wallis_Seq . x ) by FUNCT_1:def 3;
hence 0 < r by A1; :: thesis: verum

end;

hence Wallis_Seq is positive-yielding by PARTFUN3:def 1; :: thesis: verum