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