let n be Nat; :: thesis: for r being real number st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n))
let r be real number ; :: thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) )
set s1 = c_n r;
set s2 = c_d r;
assume A1: for n being Nat holds (c_d r) . n <> 0 ; :: thesis: (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n))
then A2: (c_d r) . n <> 0 ;
(c_d r) . (n + 1) <> 0 by A1;
then (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1)))) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by A2, XCMPLX_1:131
.= ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by Th64 ;
hence (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) ; :: thesis: verum