reconsider F = <%(halt S)%> as NAT -defined the Instructions of S -valued non empty finite initial Function ;
take F ; :: thesis: ( F is halt-ending & F is unique-halt & F is trivial & F is really-closed )
thus F . (LastLoc F) = halt S by Lm7; :: according to COMPOS_1:def 8 :: thesis: ( F is unique-halt & F is trivial & F is really-closed )
thus for f being Nat st F . f = halt S & f in dom F holds
f = LastLoc F by Lm7; :: according to COMPOS_1:def 9 :: thesis: ( F is trivial & F is really-closed )
thus ( F is trivial & F is really-closed ) by Th46; :: thesis: verum