theorem :: CATALAN2:54

for r being Real ex Catal being Real_Sequence st
( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (r |^ n) ) & ( |.r.| < 1 / 4 implies ( Catal is absolutely_summable & Sum Catal = 1 + (r * ((Sum Catal) |^ 2)) & Sum Catal = 2 / (1 + (sqrt (1 - (4 * r)))) & ( r <> 0 implies Sum Catal = (1 - (sqrt (1 - (4 * r)))) / (2 * r) ) ) ) )