let a, b be set ; :: thesis: dom (a followed_by b) = NAT
thus dom (a followed_by b) = dom ((NAT --> b) +* (0,a))
.= dom (NAT --> b) by Th29
.= NAT ; :: thesis: verum