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

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