let n, m be Element of NAT ; for h, x being Real
for f being Function of REAL,REAL holds ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x
let h, x be Real; for f being Function of REAL,REAL holds ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x
let f be Function of REAL,REAL; ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x
defpred S1[ Nat] means for x being Real holds ((cdif (((cdif (f,h)) . m),h)) . $1) . x = ((cdif (f,h)) . (m + $1)) . x;
A1:
S1[ 0 ]
by DIFF_1:def 8;
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
((cdif (((cdif (f,h)) . m),h)) . i) . x = ((cdif (f,h)) . (m + i)) . x
;
S1[i + 1]
let x be
Real;
((cdif (((cdif (f,h)) . m),h)) . (i + 1)) . x = ((cdif (f,h)) . (m + (i + 1))) . x
(cdif (f,h)) . m is
Function of
REAL,
REAL
by DIFF_1:19;
then A4:
(cdif (((cdif (f,h)) . m),h)) . i is
Function of
REAL,
REAL
by DIFF_1:19;
A5:
(cdif (f,h)) . (m + i) is
Function of
REAL,
REAL
by DIFF_1:19;
((cdif (((cdif (f,h)) . m),h)) . (i + 1)) . x =
(cD (((cdif (((cdif (f,h)) . m),h)) . i),h)) . x
by DIFF_1:def 8
.=
(((cdif (((cdif (f,h)) . m),h)) . i) . (x + (h / 2))) - (((cdif (((cdif (f,h)) . m),h)) . i) . (x - (h / 2)))
by A4, DIFF_1:5
.=
(((cdif (f,h)) . (m + i)) . (x + (h / 2))) - (((cdif (((cdif (f,h)) . m),h)) . i) . (x - (h / 2)))
by A3
.=
(((cdif (f,h)) . (m + i)) . (x + (h / 2))) - (((cdif (f,h)) . (m + i)) . (x - (h / 2)))
by A3
.=
(cD (((cdif (f,h)) . (m + i)),h)) . x
by A5, DIFF_1:5
.=
((cdif (f,h)) . ((m + i) + 1)) . x
by DIFF_1:def 8
;
hence
((cdif (((cdif (f,h)) . m),h)) . (i + 1)) . x = ((cdif (f,h)) . (m + (i + 1))) . x
;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x
; verum