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 ;
( x in {0} implies (IncAddr ((Stop S),k)) . x = (Stop S) . x )
assume A3:
x in {0}
;
(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
;
verum
end;
hence
IncAddr ((Stop S),k) = Stop S
by A1, A2, FUNCT_1:2; verum