theorem Th14: :: DIOPHAN1:13

for n being Nat
for r being Real st r is irrational holds
r = ((((c_n r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_n r) . n)) / ((((c_d r) . (n + 1)) * ((rfs r) . (n + 2))) + ((c_d r) . n))