let n be Nat; :: thesis: for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n))
let r be Real; :: thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) )
set s1 = c_n r;
set s2 = c_d r;
set s = scf r;
assume for n being Nat holds (c_d r) . n <> 0 ; :: thesis: (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n))
then ( (c_d r) . n <> 0 & (c_d r) . (n + 2) <> 0 ) ;
then (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = ((((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2)))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) by XCMPLX_1:130
.= (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) by Th66 ;
hence (((c_n r) . (n + 2)) / ((c_d r) . (n + 2))) - (((c_n r) . n) / ((c_d r) . n)) = (((- 1) |^ n) * ((scf r) . (n + 2))) / (((c_d r) . (n + 2)) * ((c_d r) . n)) ; :: thesis: verum