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