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 `3_3 and

A3: x address_1 = f /. 1 by Def3;

f = <*mk,ml*> by A1, A2;

hence x address_1 = mk by A3, FINSEQ_4:17; :: thesis: x address_2 = ml

consider f being FinSequence of SCM-Data-Loc such that

A4: f = x `3_3 and

A5: x address_2 = f /. 2 by A1, Def4;

f = <*mk,ml*> by A1, A4;

hence x address_2 = ml by A5, FINSEQ_4:17; :: thesis: verum

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 `3_3 and

A3: x address_1 = f /. 1 by Def3;

f = <*mk,ml*> by A1, A2;

hence x address_1 = mk by A3, FINSEQ_4:17; :: thesis: x address_2 = ml

consider f being FinSequence of SCM-Data-Loc such that

A4: f = x `3_3 and

A5: x address_2 = f /. 2 by A1, Def4;

f = <*mk,ml*> by A1, A4;

hence x address_2 = ml by A5, FINSEQ_4:17; :: thesis: verum