set Fa = NAT --> 1;
reconsider F = NAT --> 1 as ManySortedSet of ;
take F ; :: thesis: ( F is halting & F is iterative & F is eventually-constant )
F . 0 = 1 by FUNCOP_1:13;
then F . 0 = F . (0 + 1) by FUNCOP_1:13;
hence F is halting by GLIB_000:def 56; :: thesis: ( F is iterative & F is eventually-constant )

now

let n, k be Nat; :: thesis: ( F . n = F . k implies F . (n + 1) = F . (k + 1) )
assume F . n = F . k ; :: thesis: F . (n + 1) = F . (k + 1)
( F . (n + 1) = 1 & F . (k + 1) = 1 ) by FUNCOP_1:13;
hence F . (n + 1) = F . (k + 1) ; :: thesis: verum

end;

hence F is iterative by Def15; :: thesis: F is eventually-constant

now

let n be Nat; :: thesis: ( 0 <= n implies F . 0 = F . n )
assume 0 <= n ; :: thesis: F . 0 = F . n
n in NAT by ORDINAL1:def 13;
then ( F . 0 = 1 & F . n = 1 ) by FUNCOP_1:13;
hence F . 0 = F . n ; :: thesis: verum

end;

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