theorem Th64: :: REAL_3:64

for n being Nat
for r being Real holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n