theorem Th7: :: DIFF_1:7

for n being Nat
for h, r, x being Real
for f being Function of REAL,REAL holds ((fdif ((r (#) f),h)) . (n + 1)) . x = r * (((fdif (f,h)) . (n + 1)) . x)