:: deftheorem defines difference NUMBER06:def 5 :
for f being Arithmetic_Progression holds difference f = (f . 1) - (f . 0);