:: deftheorem defines cD DIFF_1:def 5 :
for f being PartFunc of REAL,REAL
for h being Real holds cD (f,h) = (Shift (f,(h / 2))) - (Shift (f,(- (h / 2))));