thus ( IT is halt-free implies for x being Nat st x in dom IT holds
IT . x <> halt S ) by FUNCT_1:3; :: thesis: ( ( for x being Nat st x in dom IT holds
IT . x <> halt S ) implies IT is halt-free )
assume A1: 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 11 :: thesis: contradiction
then consider x being object such that
A2: x in dom IT and
A3: halt S = IT . x by FUNCT_1:def 3;
thus contradiction by A2, A3, A1; :: thesis: verum