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

end;

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