let i1 be Element of NAT ; :: thesis: AddressPart (goto i1) = <*i1*>
thus AddressPart (goto i1) = [6,<*i1*>] `2 by Th14
.= <*i1*> by MCART_1:def 2 ; :: thesis: verum