theorem :: DIFF_3:8

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((bdif (f1,h)) . (n + 1)) . x)) + (((bdif (f2,h)) . (n + 1)) . x)