theorem Th123: :: FUNCT_7:124

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