let Gs be ManySortedSet of NAT ; :: thesis: ( Gs is halting & Gs is iterative implies Gs is eventually-constant )
assume that
A1: Gs is halting and
A2: Gs is iterative ; :: thesis: Gs is eventually-constant
set GL = Gs .Lifespan() ;
defpred S₁[ Nat] means Gs . (Gs .Lifespan()) = Gs . ((Gs .Lifespan()) + $1);
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then Gs . ((Gs .Lifespan()) + 1) = Gs . (((Gs .Lifespan()) + k) + 1) by A2;
hence S₁[k + 1] by A1, GLIB_000:def 56; :: thesis: verum

end;

A4: S₁[ 0 ] ;
A5: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A3);

now :: thesis: for n being Nat st Gs .Lifespan() <= n holds
Gs . (Gs .Lifespan()) = Gs . n

let n be Nat; :: thesis: ( Gs .Lifespan() <= n implies Gs . (Gs .Lifespan()) = Gs . n )
assume Gs .Lifespan() <= n ; :: thesis: Gs . (Gs .Lifespan()) = Gs . n
then ex i being Nat st (Gs .Lifespan()) + i = n by NAT_1:10;
hence Gs . (Gs .Lifespan()) = Gs . n by A5; :: thesis: verum

end;

hence Gs is eventually-constant ; :: thesis: verum