let r be Real; :: thesis: ( (scf r) . 1 > 0 implies for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) )
assume A1: (scf r) . 1 > 0 ; :: thesis: for n being Nat holds (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
let n be Nat; :: thesis: (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1))
set s1 = c_d r;
set s = scf r;
set m = ((scf r) . (n + 2)) * ((c_d r) . (n + 1));
((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by Def6;
then ((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) > 0 by A1, Th52;
then (((c_d r) . (n + 2)) - (((scf r) . (n + 2)) * ((c_d r) . (n + 1)))) + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) > 0 + (((scf r) . (n + 2)) * ((c_d r) . (n + 1))) by XREAL_1:6;
hence (c_d r) . (n + 2) > ((scf r) . (n + 2)) * ((c_d r) . (n + 1)) ; :: thesis: verum