let m, n be Element of NAT ; :: thesis: for h, x being Real
for f being Function of REAL ,REAL holds ((cdif ((cdif f,h) . m),h) . n) . x = ((cdif f,h) . (m + n)) . x
let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds ((cdif ((cdif f,h) . m),h) . n) . x = ((cdif f,h) . (m + n)) . x
let f be Function of REAL ,REAL ; :: thesis: ((cdif ((cdif f,h) . m),h) . n) . x = ((cdif f,h) . (m + n)) . x
defpred S₁[ Nat] means for x being Real holds ((cdif ((cdif f,h) . m),h) . $1) . x = ((cdif f,h) . (m + $1)) . x;
A1: S₁[ 0 ] by DIFF_1:def 8;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: for x being Real holds ((cdif ((cdif f,h) . m),h) . i) . x = ((cdif f,h) . (m + i)) . x ; :: thesis: S₁[i + 1]
let x be Real; :: thesis: ((cdif ((cdif f,h) . m),h) . (i + 1)) . x = ((cdif f,h) . (m + (i + 1))) . x
(cdif f,h) . m is Function of REAL ,REAL by DIFF_1:19;
then A4: (cdif ((cdif f,h) . m),h) . i is Function of REAL ,REAL by DIFF_1:19;
A5: (cdif f,h) . (m + i) is Function of REAL ,REAL by DIFF_1:19;
((cdif ((cdif f,h) . m),h) . (i + 1)) . x = (cD ((cdif ((cdif f,h) . m),h) . i),h) . x by DIFF_1:def 8
.= (((cdif ((cdif f,h) . m),h) . i) . (x + (h / 2))) - (((cdif ((cdif f,h) . m),h) . i) . (x - (h / 2))) by A4, DIFF_1:5
.= (((cdif f,h) . (m + i)) . (x + (h / 2))) - (((cdif ((cdif f,h) . m),h) . i) . (x - (h / 2))) by A3
.= (((cdif f,h) . (m + i)) . (x + (h / 2))) - (((cdif f,h) . (m + i)) . (x - (h / 2))) by A3
.= (cD ((cdif f,h) . (m + i)),h) . x by A5, DIFF_1:5
.= ((cdif f,h) . ((m + i) + 1)) . x by DIFF_1:def 8 ;
hence ((cdif ((cdif f,h) . m),h) . (i + 1)) . x = ((cdif f,h) . (m + (i + 1))) . x ; :: thesis: verum

end;

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