theorem Th50: :: WALLIS01:50

for seq being positive-yielding Real_Sequence st seq is convergent holds
( sqrt seq is convergent & lim (sqrt seq) = sqrt (lim seq) )