:: deftheorem defines bD DIFF_1:def 4 :
for f being PartFunc of REAL,REAL
for h being Real holds bD (f,h) = f - (Shift (f,(- h)));