for n being Nat
for r being Real holds
( dom ((#Z n) / ((#Z 0) + (#Z 2))) = REAL & (#Z n) / ((#Z 0) + (#Z 2)) is continuous & ((#Z n) / ((#Z 0) + (#Z 2))) . r = (r |^ n) / (1 + (r ^2)) )