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