let Gs be ManySortedSet of ; :: thesis: ( Gs is halting & Gs is iterative implies Gs is eventually-constant )
assume A1: ( Gs is halting & Gs is iterative ) ; :: thesis: Gs is eventually-constant
set GL = Gs .Lifespan() ;
defpred S₁[ Nat] means Gs . (Gs .Lifespan() ) = Gs . ((Gs .Lifespan() ) + $1);
A2: S₁[ 0 ] ;
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 A4: S₁[k] ; :: thesis: S₁[k + 1]
Gs . ((Gs .Lifespan() ) + 1) = Gs . (((Gs .Lifespan() ) + k) + 1) by A1, A4, Def15;
hence S₁[k + 1] by A1, GLIB_000:def 57; :: thesis: verum

end;

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

now

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

end;

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