let n be Nat; for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
let h, x be Real; for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
let f be Function of REAL,REAL; ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
defpred S1[ Nat] means ((bdif (f,h)) . ($1 + 1)) . x = (((bdif (f,h)) . $1) . x) - (((bdif (f,h)) . $1) . (x - h));
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume
((bdif (f,h)) . (i + 1)) . x = (((bdif (f,h)) . i) . x) - (((bdif (f,h)) . i) . (x - h))
;
S1[i + 1]
A2:
(bdif (f,h)) . (i + 1) is
Function of
REAL,
REAL
by DIFF_1:12;
((bdif (f,h)) . (i + 2)) . x =
((bdif (f,h)) . ((i + 1) + 1)) . x
.=
(bD (((bdif (f,h)) . (i + 1)),h)) . x
by DIFF_1:def 7
.=
(((bdif (f,h)) . (i + 1)) . x) - (((bdif (f,h)) . (i + 1)) . (x - h))
by A2, DIFF_1:4
;
hence
S1[
i + 1]
;
verum
end;
A3:
S1[ 0 ]
by Th47;
for n being Nat holds S1[n]
from NAT_1:sch 2(A3, A1);
hence
((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
; verum