theorem Th36: :: WALLIS01:39

for n being Nat st n >= 2 holds
((n -' 1) / n) * ('I' . (n -' 2)) = 'I' . n