let n be Nat; :: thesis: for r being real number st n >= 1 holds
(scf r) . n >= 0
let r be real number ; :: thesis: ( n >= 1 implies (scf r) . n >= 0 )
defpred S₂[ Nat] means (scf r) . $1 >= 0 ;
A1: S₂[1]

proof

A2: (scf r) . 1 = [\((rfs r) . (0 + 1))/] by Def5
.= [\(1 / (frac ((rfs r) . 0 )))/] by Def4
.= [\(1 / (frac r))/] by Def4 ;
[\r/] <= r by INT_1:def 4;
then frac r >= 0 by XREAL_1:50;
then 1 / (frac r) >= 0 ;
then A3: (1 / (frac r)) - 1 >= 0 - 1 by XREAL_1:11;
(scf r) . 1 > (1 / (frac r)) - 1 by A2, INT_1:def 4;
then ((scf r) . 1) - (- 1) > ((1 / (frac r)) - 1) - ((1 / (frac r)) - 1) by A3, XREAL_1:16;
then (((scf r) . 1) - (- 1)) + (- 1) > 0 + (- 1) by XREAL_1:10;
then (scf r) . 1 >= (- 1) + 1 by INT_1:20;
hence S₂[1] ; :: thesis: verum

end;

A4: for n being Nat st n >= 1 & S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₂[n] implies S₂[n + 1] )
assume n >= 1 ; :: thesis: ( not S₂[n] or S₂[n + 1] )
A5: (scf r) . (n + 1) = [\((rfs r) . (n + 1))/] by Def5
.= [\(1 / (frac ((rfs r) . n)))/] by Def4 ;
[\((rfs r) . n)/] <= (rfs r) . n by INT_1:def 4;
then frac ((rfs r) . n) >= 0 by XREAL_1:50;
then 1 / (frac ((rfs r) . n)) >= 0 ;
then A6: (1 / (frac ((rfs r) . n))) - 1 >= 0 - 1 by XREAL_1:11;
(scf r) . (n + 1) > (1 / (((rfs r) . n) - [\((rfs r) . n)/])) - 1 by A5, INT_1:def 4;
then ((scf r) . (n + 1)) - (- 1) > ((1 / (frac ((rfs r) . n))) - 1) - ((1 / (frac ((rfs r) . n))) - 1) by A6, XREAL_1:16;
then (((scf r) . (n + 1)) - (- 1)) + (- 1) > 0 + (- 1) by XREAL_1:10;
then (scf r) . (n + 1) >= (- 1) + 1 by INT_1:20;
hence ( not S₂[n] or S₂[n + 1] ) ; :: thesis: verum

end;

for n being Nat st n >= 1 holds
S₂[n] from NAT_1:sch 8(A1, A4);
hence ( n >= 1 implies (scf r) . n >= 0 ) ; :: thesis: verum