theorem Th124: :: FUNCT_7:125

for a, b, c being set holds (a,b) followed_by c = (a followed_by c) +* (1,b)