let N be non empty with_non-empty_elements set ; :: thesis: for k being natural number
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N holds IncAddr ((Stop S),k) = Stop S
let k be natural number ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N holds IncAddr ((Stop S),k) = Stop S
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-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