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