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