let I be non empty preProgram of S; :: thesis: ( I is halt-ending implies not I is halt-free )
assume I is halt-ending ; :: thesis: not I is halt-free
then A1: I . (LastLoc I) = halt S ;
LastLoc I in dom I by VALUED_1:30;
hence halt S in rng I by A1, FUNCT_1:3; :: according to COMPOS_1:def 11 :: thesis: verum