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

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