thus ( IT is halt-free implies for x being Nat st x in dom IT holds
IT . x <> halt S ) :: thesis: ( ( for x being 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 Nat st x in dom IT holds
IT . x <> halt S
let x be 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 by ORDINAL1:def 12;
IT . n in rng IT by A2, FUNCT_1:3;
hence IT . x <> halt S by A1, Def7; :: thesis: verum

end;

assume A3: for x being 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 3 :: thesis: contradiction
then consider x being set such that
A4: x in dom IT and
A5: halt S = IT . x by FUNCT_1:def 3;
thus contradiction by A4, A5, A3; :: thesis: verum