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