let i1 be Instruction-Location of SCM+FSA ; :: thesis: AddressPart (goto i1) = <*i1*>
thus AddressPart (goto i1) = [6,<*i1*>] `2 by Th14
.= <*i1*> by MCART_1:def 2 ; :: thesis: verum