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 Z: 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 ZZ: x in dom IT ; :: thesis: IT . x <> halt S
reconsider n = x as Element of NAT ;
IT . n in rng IT by ZZ, FUNCT_1:12;
hence IT . x <> halt S by Z, COMPOS_1:def 7; :: thesis: verum

end;

assume Z: 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
W1: x in dom IT and
W2: halt S = IT . x by FUNCT_1:def 5;
dom IT c= NAT by RELAT_1:def 18;
then x in NAT by W1;
hence contradiction by W1, W2, Z; :: thesis: verum