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

proof

let x be Real; :: thesis: ((bdif f,h) . 0 ) . x = ((cdif f,h) . 0 ) . (x - ((0 / 2) * h))
((bdif f,h) . 0 ) . x = f . x by DIFF_1:def 7
.= ((cdif f,h) . 0 ) . (x - ((0 / 2) * h)) by DIFF_1:def 8 ;
hence ((bdif f,h) . 0 ) . x = ((cdif f,h) . 0 ) . (x - ((0 / 2) * h)) ; :: 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 / 2) * h)) ; :: thesis: S₁[i + 1]
let x be Real; :: thesis: ((bdif f,h) . (i + 1)) . x = ((cdif f,h) . (i + 1)) . (x - (((i + 1) / 2) * h))
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 / 2) * h))) - (((bdif f,h) . i) . (x - h)) by A3
.= (((cdif f,h) . i) . (x - ((i / 2) * h))) - (((cdif f,h) . i) . ((x - h) - ((i / 2) * h))) by A3
.= (((cdif f,h) . i) . ((x - (((i + 1) / 2) * h)) + (h / 2))) - (((cdif f,h) . i) . ((x - (((i + 1) / 2) * h)) - (h / 2)))
.= (cD ((cdif f,h) . i),h) . (x - (((i + 1) / 2) * h)) by A5, DIFF_1:5
.= ((cdif f,h) . (i + 1)) . (x - (((i + 1) / 2) * h)) by DIFF_1:def 8 ;
hence ((bdif f,h) . (i + 1)) . x = ((cdif f,h) . (i + 1)) . (x - (((i + 1) / 2) * h)) ; :: 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 / 2) * h)) implies ((bdif f,h) . n) . x = ((cdif f,h) . n) . (x - ((n / 2) * h)) ) ; :: thesis: verum