theorem :: WALLIS01:52

for n being non zero Nat holds (sqrt Wallis_Seq) . (n -' 1) = ((sqrt n) * ((2 * n) !)) / ((4 |^ n) * ((n !) |^ 2))