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 S₂[ 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 S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A7: S₂[n] ; :: thesis: S₂[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
.= 0 ;
then (scf (1 / i)) . (0 + 2) = [\0/] by Def4
.= 0 ;
then A9: S₂[ 0 ] by A8;
A10: for n being Nat holds S₂[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; :: thesis: verum