let x be Element of SCM-Instr ; :: thesis: for mk being Nat

for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds

x jump_address = mk

let mk be Nat; :: thesis: for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds

x jump_address = mk

let I be Element of Segm 9; :: thesis: ( x = [I,<*mk*>,{}] implies x jump_address = mk )

assume A1: x = [I,<*mk*>,{}] ; :: thesis: x jump_address = mk

then consider f being FinSequence of NAT such that

A2: f = x `2_3 and

A3: x jump_address = f /. 1 by Def5;

reconsider mk = mk as Element of NAT by ORDINAL1:def 12;

f = <*mk*> by A1, A2;

hence x jump_address = mk by A3, FINSEQ_4:16; :: thesis: verum

for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds

x jump_address = mk

let mk be Nat; :: thesis: for I being Element of Segm 9 st x = [I,<*mk*>,{}] holds

x jump_address = mk

let I be Element of Segm 9; :: thesis: ( x = [I,<*mk*>,{}] implies x jump_address = mk )

assume A1: x = [I,<*mk*>,{}] ; :: thesis: x jump_address = mk

then consider f being FinSequence of NAT such that

A2: f = x `2_3 and

A3: x jump_address = f /. 1 by Def5;

reconsider mk = mk as Element of NAT by ORDINAL1:def 12;

f = <*mk*> by A1, A2;

hence x jump_address = mk by A3, FINSEQ_4:16; :: thesis: verum