let n be Nat; :: thesis: for r being Real st n >= 1 holds
(scf r) . n >= 0
let r be Real; :: thesis: ( n >= 1 implies (scf r) . n >= 0 )
defpred S2[ Nat] means (scf r) . $1 >= 0 ;
[\r/] <= r by INT_1:def 6;
then frac r >= 0 by XREAL_1:48;
then A1: (1 / (frac r)) - 1 >= 0 - 1 by XREAL_1:9;
A2: for n being Nat st n >= 1 & S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( n >= 1 & S2[n] implies S2[n + 1] )
assume n >= 1 ; :: thesis: ( not S2[n] or S2[n + 1] )
[\((rfs r) . n)/] <= (rfs r) . n by INT_1:def 6;
then frac ((rfs r) . n) >= 0 by XREAL_1:48;
then A3: (1 / (frac ((rfs r) . n))) - 1 >= 0 - 1 by XREAL_1:9;
(scf r) . (n + 1) = [\((rfs r) . (n + 1))/] by Def4
.= [\(1 / (frac ((rfs r) . n)))/] by Def3 ;
then (scf r) . (n + 1) > (1 / (((rfs r) . n) - [\((rfs r) . n)/])) - 1 by INT_1:def 6;
then ((scf r) . (n + 1)) - (- 1) > ((1 / (frac ((rfs r) . n))) - 1) - ((1 / (frac ((rfs r) . n))) - 1) by A3, XREAL_1:14;
hence ( not S2[n] or S2[n + 1] ) by INT_1:7; :: thesis: verum
end;
(scf r) . 1 = [\((rfs r) . (0 + 1))/] by Def4
.= [\(1 / (frac ((rfs r) . 0)))/] by Def3
.= [\(1 / (frac r))/] by Def3 ;
then (scf r) . 1 > (1 / (frac r)) - 1 by INT_1:def 6;
then ((scf r) . 1) - (- 1) > ((1 / (frac r)) - 1) - ((1 / (frac r)) - 1) by A1, XREAL_1:14;
then A4: S2[1] by INT_1:7;
for n being Nat st n >= 1 holds
S2[n] from NAT_1:sch 8(A4, A2);
 hence ( n >= 1 implies (scf r) . n >= 0 ) ; :: thesis: verum