reconsider roku = 6 as Element of Segm 9 by NAT_1:45;
let loc be Element of NAT ; :: thesis: (@ (SCM-goto loc)) jump_address = loc
reconsider mk = loc as Element of NAT ;
@ (SCM-goto loc) = [roku,<*mk*>] ;
hence (@ (SCM-goto loc)) jump_address = loc by AMI_2:24; :: thesis: verum