let n be Nat; :: thesis: for r being Real holds
( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) )
let r be Real; :: thesis: ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) )
set x = r - ((scf r) . 0);
defpred S₂[ Nat] means ( (rfs (1 / (r - ((scf r) . 0)))) . $1 = (rfs r) . ($1 + 1) & (scf (1 / (r - ((scf r) . 0)))) . $1 = (scf r) . ($1 + 1) );
A1: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
hence (rfs (1 / (r - ((scf r) . 0)))) . (n + 1) = 1 / (frac ((rfs r) . (n + 1))) by Def3
.= (rfs r) . ((n + 1) + 1) by Def3 ;
:: thesis: (scf (1 / (r - ((scf r) . 0)))) . (n + 1) = (scf r) . ((n + 1) + 1)
hence (scf (1 / (r - ((scf r) . 0)))) . (n + 1) = [\((rfs r) . ((n + 1) + 1))/] by Def4
.= (scf r) . ((n + 1) + 1) by Def4 ;
:: thesis: verum

end;

A2: (rfs (1 / (r - ((scf r) . 0)))) . 0 = 1 / (r - ((scf r) . 0)) by Def3
.= 1 / (((rfs r) . 0) - ((scf r) . 0)) by Def3
.= 1 / (frac ((rfs r) . 0)) by Def4
.= (rfs r) . (0 + 1) by Def3 ;
then (scf (1 / (r - ((scf r) . 0)))) . 0 = [\((rfs r) . 1)/] by Def4
.= (scf r) . (0 + 1) by Def4 ;
then A3: S₂[ 0 ] by A2;
for n being Nat holds S₂[n] from NAT_1:sch 2(A3, A1);
hence ( (rfs (1 / (r - ((scf r) . 0)))) . n = (rfs r) . (n + 1) & (scf (1 / (r - ((scf r) . 0)))) . n = (scf r) . (n + 1) ) ; :: thesis: verum