let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) )
assume A1: for n being Nat holds (scf r) . n <> 0 ; :: thesis: for n being Nat holds 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2)
let n be Nat; :: thesis: 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2)
set s = scf r;
set s2 = c_d r;
(scf r) . 1 <> 0 by A1;
then (scf r) . 1 > 0 by Th38;
then A2: (c_d r) . n > 0 by Th52;
( n + 1 >= 1 + 0 & (scf r) . (n + 1) <> 0 ) by A1, XREAL_1:7;
then ((scf r) . (n + 1)) * (((c_d r) . n) ^2) >= 1 * (((c_d r) . n) ^2) by A2, Th40, XREAL_1:64;
hence 1 / (((scf r) . (n + 1)) * (((c_d r) . n) ^2)) <= 1 / (((c_d r) . n) ^2) by A2, SQUARE_1:12, XREAL_1:118; :: thesis: verum