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

now :: thesis: for n, k being Nat st F . n = F . k holds
F . (n + 1) = F . (k + 1)

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 by FUNCOP_1:7;
hence F . (n + 1) = F . (k + 1) by FUNCOP_1:7; :: thesis: verum

end;

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

now :: thesis: for n being Nat st 0 <= n holds
F . 0 = F . n

let n be Nat; :: thesis: ( 0 <= n implies F . 0 = F . n )
assume 0 <= n ; :: thesis: F . 0 = F . n
A1: F . 0 = 1 by FUNCOP_1:7;
n in NAT by ORDINAL1:def 12;
hence F . 0 = F . n by A1, FUNCOP_1:7; :: thesis: verum

end;

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