let k be natural number ; :: thesis: for S being standard-ins homogeneous regular J/A-independent proper-halt COM-Struct holds IncAddr ((Stop S),k) = Stop S
let S be standard-ins homogeneous regular J/A-independent proper-halt COM-Struct ; :: thesis: IncAddr ((Stop S),k) = Stop S
A1: dom (IncAddr ((Stop S),k)) = dom (Stop S) by Def40
.= {0} by Lm12 ;
A2: dom (Stop S) = {0} by Lm12;
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 6
.= halt S by FUNCOP_1:72 ;
thus (IncAddr ((Stop S),k)) . x = IncAddr (((Stop S) /. 0),k) by A2, A3, A4, Def40
.= halt S by A5, Th92
.= (Stop S) . x by A4, FUNCOP_1:72 ; :: thesis: verum

end;

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