let I be Element of Segm 14; :: thesis: for x being Element of SCMPDS-Instr
for mk being Element of SCM-Data-Loc st x = [I,<*mk*>] holds
x address_1 = mk
let x be Element of SCMPDS-Instr ; :: thesis: for mk being Element of SCM-Data-Loc st x = [I,<*mk*>] holds
x address_1 = mk
let mk be Element of SCM-Data-Loc ; :: thesis: ( x = [I,<*mk*>] implies x address_1 = mk )
assume A1: x = [I,<*mk*>] ; :: thesis: x address_1 = mk
then consider f being FinSequence of SCM-Data-Loc such that
A2: ( f = x `2 & x address_1 = f /. 1 ) by Def10;
f = <*mk*> by A1, A2, MCART_1:7;
hence x address_1 = mk by A2, FINSEQ_4:25; :: thesis: verum