:: deftheorem defines odd-seq WALLIS01:def 2 :
for m being non zero Nat holds odd-seq m = (even-seq m) + ((dom (even-seq m)) --> (- 1));