let n be Element of NAT ; 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; 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; ( ((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 S1[ Nat] means for x being Real holds ((bdif (f,h)) . $1) . x = ((cdif (f,h)) . $1) . (x - (($1 / 2) * h));
A1:
S1[ 0 ]
A2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A3:
for
x being
Real holds
((bdif (f,h)) . i) . x = ((cdif (f,h)) . i) . (x - ((i / 2) * h))
;
S1[i + 1]
let x be
Real;
((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))
;
verum
end;
for n being Nat holds S1[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)) )
; verum