let n be Nat; :: thesis: for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
let f be Function of REAL,REAL; :: thesis: ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
defpred S₁[ Nat] means ((fdif (f,h)) . ($1 + 1)) . x = (((fdif (f,h)) . $1) . (x + h)) - (((fdif (f,h)) . $1) . x);
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 ((fdif (f,h)) . (i + 1)) . x = (((fdif (f,h)) . i) . (x + h)) - (((fdif (f,h)) . i) . x) ; :: thesis: S₁[i + 1]
A2: (fdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:2;
((fdif (f,h)) . (i + 2)) . x = ((fdif (f,h)) . ((i + 1) + 1)) . x
.= (fD (((fdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def 6
.= (((fdif (f,h)) . (i + 1)) . (x + h)) - (((fdif (f,h)) . (i + 1)) . x) by A2, DIFF_1:3 ;
hence S₁[i + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ] by Th40;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) ; :: thesis: verum