let I be Element of Segm 15; :: 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 `3_3 and
A3: x address_1 = f /. 1 by Def2;
f = <*mk*> by A1, A2;
hence x address_1 = mk by A3, FINSEQ_4:16; :: thesis: verum