reconsider F = <%(halt S)%> as non empty NAT -defined the Instructions of S -valued initial FinPartState of ;
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 25 :: 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 Lm7; :: according to COMPOS_1:def 26 :: thesis: F is trivial
thus F is trivial ; :: thesis: verum