let n be Nat; :: thesis: for r being Real st ( for n being Nat holds (scf r) . n = 0 ) holds
(rfs r) . n = 0
let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n = 0 ) implies (rfs r) . n = 0 )
assume that
A1: for n being Nat holds (scf r) . n = 0 and
A2: (rfs r) . n <> 0 ; :: thesis: contradiction
A3: (scf r) . n = 0 by A1;
set x = (rfs r) . n;
A4: (scf r) . n = [\((rfs r) . n)/] by Def4;
per cases ( (rfs r) . n < 0 or (rfs r) . n >= 1 or ( 0 < (rfs r) . n & (rfs r) . n < 1 ) ) by A2;
suppose (rfs r) . n < 0 ; :: thesis: contradiction
hence contradiction by A3, A4, INT_1:def 6; :: thesis: verum
end;
suppose (rfs r) . n >= 1 ; :: thesis: contradiction
hence contradiction by A3, A4, INT_1:54; :: thesis: verum
end;
suppose ( 0 < (rfs r) . n & (rfs r) . n < 1 ) ; :: thesis: contradiction
then A5: 1 / ((rfs r) . n) > 1 by Th1;
A6: ( (scf r) . (n + 1) = 0 & (scf r) . (n + 1) = [\((rfs r) . (n + 1))/] ) by A1, Def4;
(rfs r) . (n + 1) = 1 / (frac ((rfs r) . n)) by Def3
.= 1 / (((rfs r) . n) - ((scf r) . n)) by Def4
.= 1 / (((rfs r) . n) - 0) by A1
.= 1 / ((rfs r) . n) ;
hence contradiction by A5, A6, INT_1:54; :: thesis: verum
end;
end;