let Gs be iterative eventually-constant ManySortedSet of NAT ; :: thesis: for n being Nat st Gs .Lifespan() <= n holds
Gs . (Gs .Lifespan()) = Gs . n
set GL = Gs .Lifespan() ;
defpred S₁[ Nat] means Gs . (Gs .Lifespan()) = Gs . ((Gs .Lifespan()) + $1);
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 A1: ex i being Nat st (Gs .Lifespan()) + i = n by NAT_1:10;
A2: 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 Def5;
hence S₁[k + 1] by GLIB_000:def 56; :: thesis: verum

end;

A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A2);
hence Gs . (Gs .Lifespan()) = Gs . n by A1; :: thesis: verum