:: deftheorem defines ax_+_b STIRLIN1:def 2 :
for a, b being Real holds ax_+_b (a,b) = AffineMap (a,b);