:: deftheorem defines [** HAHNBAN1:def 1 :
for x, y being Real holds [**x,y**] = x + (y * <i>);