let
s
be
SCM-State
;
:: thesis:
for
u
,
v
being
natural
Number
holds
(
SCM-Chg
(
s
,
u
)
)
.
v
=
s
.
v
let
u
,
v
be
natural
Number
;
:: thesis:
(
SCM-Chg
(
s
,
u
)
)
.
v
=
s
.
v
not
v
in
dom
(
NAT
.-->
u
)
by
TARSKI:def 1
;
hence
(
SCM-Chg
(
s
,
u
))
.
v
=
s
.
v
by
FUNCT_4:11
;
:: thesis:
verum