let loc be Instruction-Location of SCM ; :: thesis: (@ (goto loc)) jump_address = loc
reconsider roku = 6 as Element of Segm 9 by GR_CY_1:10;
reconsider mk = loc as Element of NAT by AMI_1:def 4;
@ (goto loc) = [roku,<*mk*>] ;
hence (@ (goto loc)) jump_address = loc by AMI_2:24; :: thesis: verum