let n be Nat; for h being Real
for f being Function of REAL,REAL st f is constant holds
for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0
let h be Real; for f being Function of REAL,REAL st f is constant holds
for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0
let f be Function of REAL,REAL; ( f is constant implies for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0 )
assume A1:
f is constant
; for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0
A2:
for x being Real holds (f . (x + h)) - (f . x) = 0
for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0
proof
defpred S1[
Nat]
means for
x being
Real holds
((fdif (f,h)) . ($1 + 1)) . x = 0 ;
A4:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
for
x being
Real holds
((fdif (f,h)) . (k + 1)) . x = 0
;
S1[k + 1]
let x be
Real;
((fdif (f,h)) . ((k + 1) + 1)) . x = 0
A6:
((fdif (f,h)) . (k + 1)) . (x + h) = 0
by A5;
A7:
(fdif (f,h)) . (k + 1) is
Function of
REAL,
REAL
by Th2;
((fdif (f,h)) . (k + 2)) . x =
((fdif (f,h)) . ((k + 1) + 1)) . x
.=
(fD (((fdif (f,h)) . (k + 1)),h)) . x
by Def6
.=
(((fdif (f,h)) . (k + 1)) . (x + h)) - (((fdif (f,h)) . (k + 1)) . x)
by A7, Th3
.=
0 - 0
by A5, A6
.=
0
;
hence
((fdif (f,h)) . ((k + 1) + 1)) . x = 0
;
verum
end;
A8:
S1[
0 ]
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A8, A4);
hence
for
x being
Real holds
((fdif (f,h)) . (n + 1)) . x = 0
;
verum
end;
hence
for x being Real holds ((fdif (f,h)) . (n + 1)) . x = 0
; verum