let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting standard AMI-Struct of N holds 0 .--> (halt S) is really-closed
let S be non empty IC-Ins-separated halting standard AMI-Struct of N; :: thesis: 0 .--> (halt S) is really-closed
reconsider F = 0 .--> (halt S) as NAT -defined the Instructions of S -valued finite Function ;
let l be Element of NAT ; :: according to AMISTD_1:def 9 :: thesis: ( l in dom (0 .--> (halt S)) implies NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S)) )
assume A1: l in dom (0 .--> (halt S)) ; :: thesis: NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S))
A2: dom F = {0} by FUNCOP_1:13;
then A3: l = 0 by A1, TARSKI:def 1;
F /. l = F . l by A1, PARTFUN1:def 6
.= halt S by A3, FUNCOP_1:72 ;
hence NIC (((0 .--> (halt S)) /. l),l) c= dom (0 .--> (halt S)) by A2, A3, Th15; :: thesis: verum