let n be Nat; :: thesis: for i being Integer st i > 1 holds
( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 )
let i be Integer; :: thesis: ( i > 1 implies ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) )
set r = 1 / i;
defpred S2[ Nat] means ( (rfs (1 / i)) . ($1 + 2) = 0 & (scf (1 / i)) . ($1 + 2) = 0 );
assume A1: i > 1 ; :: thesis: ( (rfs (1 / i)) . 1 = i & (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 )
then A2: 1 / i < 0 + 1 by XREAL_1:189;
A3: [\((rfs (1 / i)) . 0)/] = [\(1 / i)/] by Def3
.= 0 by A1, A2, Th2 ;
thus A4: (rfs (1 / i)) . 1 = (rfs (1 / i)) . (0 + 1)
.= 1 / (frac ((rfs (1 / i)) . 0)) by Def3
.= 1 / ((1 / i) - 0) by A3, Def3
.= i ; :: thesis: ( (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 )
then A5: (scf (1 / i)) . 1 = [\i/] by Def4;
A6: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A7: S2[n] ; :: thesis: S2[n + 1]
thus (rfs (1 / i)) . ((n + 1) + 2) = (rfs (1 / i)) . ((n + 2) + 1)
.= 1 / (frac ((rfs (1 / i)) . (n + 2))) by Def3
.= 1 / (0 - 0) by A7
.= 0 ; :: thesis: (scf (1 / i)) . ((n + 1) + 2) = 0
hence (scf (1 / i)) . ((n + 1) + 2) = [\0/] by Def4
.= 0 ;
:: thesis: verum
end;
A8: (rfs (1 / i)) . (0 + 2) = (rfs (1 / i)) . (1 + 1)
.= 1 / (frac ((rfs (1 / i)) . 1)) by Def3
.= 1 / (i - i) by A4, INT_1:25
.= 0 ;
then (scf (1 / i)) . (0 + 2) = [\0/] by Def4
.= 0 ;
then A9: S2[ 0 ] by A8;
A10: for n being Nat holds S2[n] from NAT_1:sch 2(A9, A6);
 (scf (1 / i)) . 0 = [\((rfs (1 / i)) . 0)/] by Def4
.= [\(1 / i)/] by Def3
.= 0 by A1, A2, Th2 ;
hence ( (rfs (1 / i)) . (n + 2) = 0 & (scf (1 / i)) . 0 = 0 & (scf (1 / i)) . 1 = i & (scf (1 / i)) . (n + 2) = 0 ) by A5, A10, INT_1:25; :: thesis: verum