theorem Th7: :: WALLIS01:10

for n being non zero Nat holds odd-seq (n + 1) = (odd-seq n) ^ <*((2 * n) + 1)*>