a followed_by b = (NAT --> b) +* (0,a) ;
hence a followed_by b is sequence of X by Th117; :: thesis: verum