set F = Stop S;
let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( l in dom (Stop S) implies NIC (((Stop S) /. l),l) c= dom (Stop S) )
assume A1: l in dom (Stop S) ; :: thesis: NIC (((Stop S) /. l),l) c= dom (Stop S)
A3: l = 0 by A1, TARSKI:def 1;
(Stop S) /. l = (Stop S) . l by A1, PARTFUN1:def 6
.= halt S by A3 ;
hence NIC (((Stop S) /. l),l) c= dom (Stop S) by A3, Th2; :: thesis: verum