thus ( IT is halt-free implies for x being Element of NAT st x in dom IT holds
IT . x <> halt S ) :: thesis: ( ( for x being Element of NAT st x in dom IT holds
IT . x <> halt S ) implies IT is halt-free )

proof

assume A1: IT is halt-free ; :: thesis: for x being Element of NAT st x in dom IT holds
IT . x <> halt S
let x be Element of NAT ; :: thesis: ( x in dom IT implies IT . x <> halt S )
assume A2: x in dom IT ; :: thesis: IT . x <> halt S
reconsider n = x as Element of NAT ;
IT . n in rng IT by A2, FUNCT_1:12;
hence IT . x <> halt S by A1, COMPOS_1:def 7; :: thesis: verum

end;

assume A3: for x being Element of NAT st x in dom IT holds
IT . x <> halt S ; :: thesis: IT is halt-free
assume halt S in rng IT ; :: according to COMPOS_1:def 7 :: thesis: contradiction
then consider x being set such that
A4: x in dom IT and
A5: halt S = IT . x by FUNCT_1:def 5;
dom IT c= NAT by RELAT_1:def 18;
hence contradiction by A4, A5, A3; :: thesis: verum