Proof: We use the first property of our assignment functions to
derive that, in our new world, 
.
is a shorthand for the result of
equating a term in the frame, 
, to the term 
.
We use the second property of our assignment function a to derive
that 
. This follows as 
is in the frame, and is true in our current world, so we have that
its value persists. We also show that 
in the
same way.
We now use the effect axiom to derive that
Finally the definition of 
, which is
in the core theory gives us
Proof: We use the first property of our assignment functions to
derive that in our new world, 
as
above.
We use the second property of our assignment functions to derive that
and as we did
previously.
We now use the frame axiom 18 to derive that
using the given fact that and . Finally the
definition of gives us