reconsider F = <%(halt S)%> as non empty NAT -defined the Instructions of S -valued finite initial Function ;
take F ; :: thesis: ( F is halt-ending & F is unique-halt & F is trivial )
thus F . (LastLoc F) = halt S by Lm7; :: according to COMPOS_1:def 8 :: thesis: ( F is unique-halt & F is trivial )
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
thus F is trivial ; :: thesis: verum