let m, n be Element of 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₁[ Element of 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 Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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 Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A1);
hence ((fdif ((fdif f,h) . m),h) . n) . x = ((fdif f,h) . (m + n)) . x ; :: thesis: verum