let n be Nat; :: thesis: for r being Real holds
( r = (rfs r) . 0 & r = ((scf r) . 0) + (1 / ((rfs r) . 1)) & (rfs r) . n = ((scf r) . n) + (1 / ((rfs r) . (n + 1))) )
let r be Real; :: thesis: ( r = (rfs r) . 0 & r = ((scf r) . 0) + (1 / ((rfs r) . 1)) & (rfs r) . n = ((scf r) . n) + (1 / ((rfs r) . (n + 1))) )
A1: (rfs r) . 1 = (rfs r) . (0 + 1)
.= 1 / (frac ((rfs r) . 0)) by REAL_3:def 3 ;
A2: frac ((rfs r) . 0) = frac r by REAL_3:def 3
.= r - ((scf r) . 0) by REAL_3:35 ;
A4: frac ((rfs r) . n) = ((rfs r) . n) - [\((rfs r) . n)/] by INT_1:def 8;
1 / ((rfs r) . (n + 1)) = 1 / (1 / (frac ((rfs r) . n))) by REAL_3:def 3
.= frac ((rfs r) . n) ;
then ((scf r) . n) + (1 / ((rfs r) . (n + 1))) = (((scf r) . n) + ((rfs r) . n)) - [\((rfs r) . n)/] by A4
.= (((scf r) . n) + ((rfs r) . n)) - ((scf r) . n) by REAL_3:def 4
.= (rfs r) . n ;
hence ( r = (rfs r) . 0 & r = ((scf r) . 0) + (1 / ((rfs r) . 1)) & (rfs r) . n = ((scf r) . n) + (1 / ((rfs r) . (n + 1))) ) by REAL_3:def 3, A2, A1; :: thesis: verum