reconsider F = (il. (S,0)) .--> (halt S) as NAT -defined the InstructionsF of S -valued non empty finite lower Function by Th25;
take F ; :: thesis: ( F is halt-ending & F is unique-halt & F is trivial )
thus F . (LastLoc F) = halt S by Lm4; :: according to AMI_WSTD:def 12 :: thesis: ( F is unique-halt & F is trivial )
thus for f being Element of NAT st F . f = halt S & f in dom F holds
f = LastLoc F by Lm4; :: according to AMI_WSTD:def 13 :: thesis: F is trivial
thus F is trivial ; :: thesis: verum