theorem Th12: :: DIFF_1:12
for h being Real
for f being Function of REAL,REAL
for n being Nat holds (bdif (f,h)) . n is Function of REAL,REAL