let n, m be Element of NAT ; :: thesis: for h, x being Real
for f being Function of REAL,REAL holds ((bdif (((bdif (f,h)) . m),h)) . n) . x = ((bdif (f,h)) . (m + n)) . x
let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((bdif (((bdif (f,h)) . m),h)) . n) . x = ((bdif (f,h)) . (m + n)) . x
let f be Function of REAL,REAL; :: thesis: ((bdif (((bdif (f,h)) . m),h)) . n) . x = ((bdif (f,h)) . (m + n)) . x
defpred S₁[ Nat] means for x being Real holds ((bdif (((bdif (f,h)) . m),h)) . $1) . x = ((bdif (f,h)) . (m + $1)) . x;
A1: S₁[ 0 ] by DIFF_1:def 7;
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 ((bdif (((bdif (f,h)) . m),h)) . i) . x = ((bdif (f,h)) . (m + i)) . x ; :: thesis: S₁[i + 1]
let x be Real; :: thesis: ((bdif (((bdif (f,h)) . m),h)) . (i + 1)) . x = ((bdif (f,h)) . (m + (i + 1))) . x
(bdif (f,h)) . m is Function of REAL,REAL by DIFF_1:12;
then A4: (bdif (((bdif (f,h)) . m),h)) . i is Function of REAL,REAL by DIFF_1:12;
A5: (bdif (f,h)) . (m + i) is Function of REAL,REAL by DIFF_1:12;
((bdif (((bdif (f,h)) . m),h)) . (i + 1)) . x = (bD (((bdif (((bdif (f,h)) . m),h)) . i),h)) . x by DIFF_1:def 7
.= (((bdif (((bdif (f,h)) . m),h)) . i) . x) - (((bdif (((bdif (f,h)) . m),h)) . i) . (x - h)) by A4, DIFF_1:4
.= (((bdif (f,h)) . (m + i)) . x) - (((bdif (((bdif (f,h)) . m),h)) . i) . (x - h)) by A3
.= (((bdif (f,h)) . (m + i)) . x) - (((bdif (f,h)) . (m + i)) . (x - h)) by A3
.= (bD (((bdif (f,h)) . (m + i)),h)) . x by A5, DIFF_1:4
.= ((bdif (f,h)) . ((m + i) + 1)) . x by DIFF_1:def 7 ;
hence ((bdif (((bdif (f,h)) . m),h)) . (i + 1)) . x = ((bdif (f,h)) . (m + (i + 1))) . x ; :: thesis: verum

end;

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