let I be Element of Segm 8; :: thesis: for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Nat st x = [I,<*mk*>,{}] holds
x jump_address = mk
let S be non empty 1-sorted ; :: thesis: for x being Element of SCM-Instr S
for mk being Nat st x = [I,<*mk*>,{}] holds
x jump_address = mk
let x be Element of SCM-Instr S; :: thesis: for mk being Nat st x = [I,<*mk*>,{}] holds
x jump_address = mk
let mk be Nat; :: thesis: ( x = [I,<*mk*>,{}] implies x jump_address = mk )
assume A1: x = [I,<*mk*>,{}] ; :: thesis: x jump_address = mk
reconsider mk = mk as Element of NAT by ORDINAL1:def 12;
x = [I,<*mk*>,{}] by A1;
then consider f being FinSequence of NAT such that
A2: f = x `2_3 and
A3: x jump_address = f /. 1 by Def4;
f = <*mk*> by A1, A2;
hence x jump_address = mk by A3, FINSEQ_4:16; :: thesis: verum