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

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