let n be Nat; :: thesis: for r being real number holds ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n))
let r be real number ; :: thesis: ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n))
(c_n r) . (n + 2) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def6;
hence ((c_n r) . (n + 2)) / ((c_d r) . (n + 2)) = ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) / ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) by Def7; :: thesis: verum