let Gs be iterative eventually-constant ManySortedSet of ; :: thesis: for n being Nat st Gs .Lifespan() <= n holds
Gs . (Gs .Lifespan() ) = Gs . n
set GL = Gs .Lifespan() ;
let n be Nat; :: thesis: ( Gs .Lifespan() <= n implies Gs . (Gs .Lifespan() ) = Gs . n )
assume A1: Gs .Lifespan() <= n ; :: thesis: Gs . (Gs .Lifespan() ) = Gs . n
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 A4, Def15;
hence S₁[k + 1] by GLIB_000:def 57; :: thesis: verum

end;

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