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