let n be Element of NAT ; :: thesis: for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2))
let h, x be Real; :: thesis: for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2))
let f be Function of REAL,REAL; :: thesis: ( ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) implies ((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2)) )
defpred S₁[ Nat] means for x being Real holds ((bdif (f,h)) . $1) . x = ((cdif (f,h)) . $1) . ((x - ((($1 - 1) / 2) * h)) - (h / 2));
A1: S₁[ 0 ]

proof

let x be Real; :: thesis: ((bdif (f,h)) . 0) . x = ((cdif (f,h)) . 0) . ((x - (((0 - 1) / 2) * h)) - (h / 2))
((bdif (f,h)) . 0) . x = f . x by DIFF_1:def 7
.= ((cdif (f,h)) . 0) . ((x - (((0 - 1) / 2) * h)) - (h / 2)) by DIFF_1:def 8 ;
hence ((bdif (f,h)) . 0) . x = ((cdif (f,h)) . 0) . ((x - (((0 - 1) / 2) * h)) - (h / 2)) ; :: thesis: verum

end;

A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: for x being Real holds ((bdif (f,h)) . i) . x = ((cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2)) ; :: thesis: S₁[i + 1]
let x be Real; :: thesis: ((bdif (f,h)) . (i + 1)) . x = ((cdif (f,h)) . (i + 1)) . ((x - ((((i + 1) - 1) / 2) * h)) - (h / 2))
A4: (bdif (f,h)) . i is Function of REAL,REAL by DIFF_1:12;
A5: (cdif (f,h)) . i is Function of REAL,REAL by DIFF_1:19;
((bdif (f,h)) . (i + 1)) . x = (bD (((bdif (f,h)) . i),h)) . x by DIFF_1:def 7
.= (((bdif (f,h)) . i) . x) - (((bdif (f,h)) . i) . (x - h)) by A4, DIFF_1:4
.= (((cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2))) - (((bdif (f,h)) . i) . (x - h)) by A3
.= (((cdif (f,h)) . i) . ((x - (((i - 1) / 2) * h)) - (h / 2))) - (((cdif (f,h)) . i) . (((x - h) - (((i - 1) / 2) * h)) - (h / 2))) by A3
.= (((cdif (f,h)) . i) . (((x - ((i / 2) * h)) - (h / 2)) + (h / 2))) - (((cdif (f,h)) . i) . (((x - ((i / 2) * h)) - (h / 2)) - (h / 2)))
.= (cD (((cdif (f,h)) . i),h)) . ((x - ((i / 2) * h)) - (h / 2)) by A5, DIFF_1:5
.= ((cdif (f,h)) . (i + 1)) . ((x - ((i / 2) * h)) - (h / 2)) by DIFF_1:def 8 ;
hence ((bdif (f,h)) . (i + 1)) . x = ((cdif (f,h)) . (i + 1)) . ((x - ((((i + 1) - 1) / 2) * h)) - (h / 2)) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ( ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) implies ((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2)) ) ; :: thesis: verum