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