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 = F . (0 + 1) ;
hence F is halting ; :: thesis: ( F is iterative & F is eventually-constant )
thus F is iterative ; :: thesis: F is eventually-constant
for n being Nat st 0 <= n holds
F . 0 = F . n by FUNCOP_1:7, ORDINAL1:def 12;
hence F is eventually-constant ; :: thesis: verum