let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N holds IncAddr (Stop S),k = Stop S
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N holds IncAddr (Stop S),k = Stop S
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins standard without_implicit_jumps regular AMI-Struct of N; :: thesis: IncAddr (Stop S),k = Stop S
A1: dom (IncAddr (Stop S),k) = dom (Stop S) by Def15
.= {(il. S,0 )} by Lm5 ;
A2: dom (Stop S) = {(il. S,0 )} by Lm5;
for x being set st x in {(il. S,0 )} holds
(IncAddr (Stop S),k) . x = (Stop S) . x

proof

let x be set ; :: thesis: ( x in {(il. S,0 )} implies (IncAddr (Stop S),k) . x = (Stop S) . x )
assume A3: x in {(il. S,0 )} ; :: thesis: (IncAddr (Stop S),k) . x = (Stop S) . x
then A4: x = il. S,0 by TARSKI:def 1;
then A5: pi (Stop S),(il. S,0 ) = (Stop S) . (il. S,0 ) by A2, A3, AMI_1:def 47
.= halt S by FUNCOP_1:87 ;
thus (IncAddr (Stop S),k) . x = IncAddr (pi (Stop S),(il. S,0 )),k by A2, A3, A4, Def15
.= halt S by A5, Th29
.= (Stop S) . x by A4, FUNCOP_1:87 ; :: thesis: verum

end;

hence IncAddr (Stop S),k = Stop S by A1, A2, FUNCT_1:9; :: thesis: verum