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