theorem Th2: :: WALLIS01:5

for n being non zero Nat
for i being Nat st i in dom (odd-seq n) holds
(odd-seq n) . i = (2 * i) - 1