theorem Th119: :: FUNCT_7:120

for a, b being set
for n being Nat st n > 0 holds
(a followed_by b) . n = b