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