theorem Th117: :: FUNCT_7:118

for a, b being set holds dom (a followed_by b) = NAT