A1: dom (IncAddr ((Stop S),k)) = dom (Stop S) by Def9
.= {0} ;
A2: dom (Stop S) = {0} ;
for x being object st x in {0} holds
(IncAddr ((Stop S),k)) . x = (Stop S) . x

proof

let x be object ; :: 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 ;
thus (IncAddr ((Stop S),k)) . x = IncAddr (((Stop S) /. 0),k) by A2, A3, A4, Def9
.= halt S by A5, COMPOS_0:4
.= (Stop S) . x by A4 ; :: thesis: verum

end;

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