let n, m be Nat; :: thesis: for h, x being Real
for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x
let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x
let f be Function of REAL,REAL; :: thesis: ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x
defpred S₁[ Nat] means for x being Real holds ((fdif (((fdif (f,h)) . m),h)) . $1) . x = ((fdif (f,h)) . (m + $1)) . x;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for x being Real holds ((fdif (((fdif (f,h)) . m),h)) . k) . x = ((fdif (f,h)) . (m + k)) . x ; :: thesis: S₁[k + 1]
let x be Real; :: thesis: ((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = ((fdif (f,h)) . (m + (k + 1))) . x
A3: (fdif (f,h)) . (m + k) is Function of REAL,REAL by Th2;
(fdif (f,h)) . m is Function of REAL,REAL by Th2;
then A4: (fdif (((fdif (f,h)) . m),h)) . k is Function of REAL,REAL by Th2;
((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = (fD (((fdif (((fdif (f,h)) . m),h)) . k),h)) . x by Def6
.= (((fdif (((fdif (f,h)) . m),h)) . k) . (x + h)) - (((fdif (((fdif (f,h)) . m),h)) . k) . x) by A4, Th3
.= (((fdif (f,h)) . (m + k)) . (x + h)) - (((fdif (((fdif (f,h)) . m),h)) . k) . x) by A2
.= (((fdif (f,h)) . (m + k)) . (x + h)) - (((fdif (f,h)) . (m + k)) . x) by A2
.= (fD (((fdif (f,h)) . (m + k)),h)) . x by A3, Th3
.= ((fdif (f,h)) . ((m + k) + 1)) . x by Def6 ;
hence ((fdif (((fdif (f,h)) . m),h)) . (k + 1)) . x = ((fdif (f,h)) . (m + (k + 1))) . x ; :: thesis: verum

end;

A5: S₁[ 0 ] by Def6;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A1);
hence ((fdif (((fdif (f,h)) . m),h)) . n) . x = ((fdif (f,h)) . (m + n)) . x ; :: thesis: verum