let x be Element of SCM-Instr ; :: thesis: for mk being Element of NAT
for I being Element of Segm 9 st x = [I,<*mk*>] holds
x jump_address = mk
let mk be Element of 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 and
A3: x jump_address = f /. 1 by Def11;
f = <*mk*> by A1, A2, MCART_1:7;
hence x jump_address = mk by A3, FINSEQ_4:25; :: thesis: verum