let n, m 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