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