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 S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: for x being Real holds ((fdif (((fdif (f,h)) . m),h)) . k) . x = ((fdif (f,h)) . (m + k)) . x ; :: thesis: S1[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
.= (((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
.= ((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: S1[ 0 ] by Def6;
for n being Nat holds S1[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