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;
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:191;
A3: 1 / i > 0 / i by A1;
A4: [\((rfs (1 / i)) . 0 )/] = [\(1 / i)/] by Def4
.= 0 by A2, A3, Th2 ;
A5: (scf (1 / i)) . 0 = [\((rfs (1 / i)) . 0 )/] by Def5
.= [\(1 / i)/] by Def4
.= 0 by A2, A3, Th2 ;
thus A6: (rfs (1 / i)) . 1 = (rfs (1 / i)) . (0 + 1)
.= 1 / (frac ((rfs (1 / i)) . 0 )) by Def4
.= 1 / ((1 / i) - 0 ) by A4, Def4
.= 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 A7: (scf (1 / i)) . 1 = [\i/] by Def5;
defpred S₂[ Nat] means ( (rfs (1 / i)) . ($1 + 2) = 0 & (scf (1 / i)) . ($1 + 2) = 0 );
A8: S₂[ 0 ]

proof

thus (rfs (1 / i)) . (0 + 2) = (rfs (1 / i)) . (1 + 1)
.= 1 / (frac ((rfs (1 / i)) . 1)) by Def4
.= 1 / (i - i) by A6, INT_1:47
.= 0 ; :: thesis: (scf (1 / i)) . (0 + 2) = 0
hence (scf (1 / i)) . (0 + 2) = [\0 /] by Def5
.= 0 ;
:: thesis: verum

end;

A9: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

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

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A9);
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, A7, INT_1:47; :: thesis: verum