let Gs be ManySortedSet of ; :: thesis: ( Gs is eventually-constant implies Gs is halting )
assume A1: Gs is eventually-constant ; :: thesis: Gs is halting
consider n being Nat such that
A2: for m being Nat st n <= m holds
Gs . n = Gs . m by A1, Def16;
n <= n + 1 by NAT_1:13;
then Gs . n = Gs . (n + 1) by A2;
hence Gs is halting by GLIB_000:def 56; :: thesis: verum