let a, b be Int-Location ; :: thesis: AddressPart (a := b) = <*a,b*>
thus AddressPart (a := b) = [1,<*a,b*>] `2 by Th9
.= <*a,b*> by MCART_1:def 2 ; :: thesis: verum