lim (sqrt Wallis_Seq) = sqrt (1 / PI) by Th48, Th50;
hence lim (sqrt Wallis_Seq) = 1 / (sqrt PI) by SQUARE_1:32, COMPTRIG:5; :: thesis: verum