let n be Nat; :: thesis: for r being Real holds (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2))
let r be Real; :: thesis: (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2))
set s1 = c_n r;
set s2 = c_d r;
set s = scf r;
(((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = (((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) by Def5
.= (((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) * ((c_d r) . n)) - (((c_n r) . n) * ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n))) by Def6
.= ((scf r) . (n + 2)) * ((((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))))
.= ((- 1) |^ n) * ((scf r) . (n + 2)) by Th64 ;
hence (((c_n r) . (n + 2)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 2))) = ((- 1) |^ n) * ((scf r) . (n + 2)) ; :: thesis: verum