let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
defpred S₁[ 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 S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume ((bdif (f,h)) . (i + 1)) . x = (((bdif (f,h)) . i) . x) - (((bdif (f,h)) . i) . (x - h)) ; :: thesis: S₁[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 S₁[i + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by Th47;
for n being Nat holds S₁[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)) ; :: thesis: verum