:: deftheorem defines [! DIFF_2:def 2 :
for f being real-valued Function
for x0, x1, x2, x3, x4, x5 being Real holds [!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);