:: deftheorem defines followed_by FUNCT_7:def 13 :
for a, b being set holds a followed_by b = (NAT --> b) +* (0,a);