theorem Th118: :: FUNCT_7:119

for a, b being set holds (a followed_by b) . 0 = a