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

proof

let x be set ; :: thesis: ( x in {0 } implies (IncAddr (Stop S),k) . x = (Stop S) . x )
assume A3: x in {0 } ; :: thesis: (IncAddr (Stop S),k) . x = (Stop S) . x
then A4: x = 0 by TARSKI:def 1;
then A5: (Stop S) /. 0 = (Stop S) . 0 by A2, A3, PARTFUN1:def 8
.= halt S by FUNCOP_1:87 ;
thus (IncAddr (Stop S),k) . x = IncAddr ((Stop 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