theorem Th120: :: FUNCT_7:121

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