theorem :: REAL_3:69

for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
for n being Nat holds |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).| = 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).|