let n, m be Nat; :: thesis: for r being Real st (rfs r) . n = 0 & n <= m holds
(rfs r) . m = 0
let r be Real; :: thesis: ( (rfs r) . n = 0 & n <= m implies (rfs r) . m = 0 )
assume that
A1: (rfs r) . n = 0 and
A2: n <= m ; :: thesis: (rfs r) . m = 0
per cases ( n = m or n < m ) by A2, XXREAL_0:1;
suppose n = m ; :: thesis: (rfs r) . m = 0
hence (rfs r) . m = 0 by A1; :: thesis: verum
end;
suppose A3: n < m ; :: thesis: (rfs r) . m = 0
defpred S2[ Nat] means ( n < $1 implies (rfs r) . $1 = 0 );
A4: for a being Nat st S2[a] holds
S2[a + 1]
proof
let a be Nat; :: thesis: ( S2[a] implies S2[a + 1] )
assume A5: S2[a] ; :: thesis: S2[a + 1]
assume n < a + 1 ; :: thesis: (rfs r) . (a + 1) = 0
then A6: n <= a by NAT_1:13;
per cases ( n = a or n < a ) by A6, XXREAL_0:1;
suppose A7: n = a ; :: thesis: (rfs r) . (a + 1) = 0
thus (rfs r) . (a + 1) = 1 / (frac ((rfs r) . a)) by Def3
.= 1 / (((rfs r) . a) - ((rfs r) . a)) by A1, A7
.= 0 ; :: thesis: verum
end;
suppose A8: n < a ; :: thesis: (rfs r) . (a + 1) = 0
thus (rfs r) . (a + 1) = 1 / (frac ((rfs r) . a)) by Def3
.= 1 / (((rfs r) . a) - ((rfs r) . a)) by A5, A8
.= 0 ; :: thesis: verum
end;
end;
end;
A9: S2[ 0 ] ;
for a being Nat holds S2[a] from NAT_1:sch 2(A9, A4);
hence (rfs r) . m = 0 by A3; :: thesis: verum
end;
end;