let I be Element of Segm 15; :: thesis: for x being Element of SCMPDS-Instr

for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let x be Element of SCMPDS-Instr ; :: thesis: for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let mk be Element of SCM-Data-Loc ; :: thesis: for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let r be Integer; :: thesis: ( x = [I,{},<*mk,r*>] implies ( x P21address = mk & x P22const = r ) )

r in INT by INT_1:def 2;

then A1: ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;

assume A2: x = [I,{},<*mk,r*>] ; :: thesis: ( x P21address = mk & x P22const = r )

then consider f being FinSequence of SCM-Data-Loc \/ INT such that

A3: f = x `3_3 and

A4: x P21address = f /. 1 by Def4;

f = <*mk,r*> by A2, A3;

hence x P21address = mk by A4, A1, FINSEQ_4:17; :: thesis: x P22const = r

consider f being FinSequence of SCM-Data-Loc \/ INT such that

A5: f = x `3_3 and

A6: x P22const = f /. 2 by A2, Def5;

f = <*mk,r*> by A2, A5;

hence x P22const = r by A1, A6, FINSEQ_4:17; :: thesis: verum

for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let x be Element of SCMPDS-Instr ; :: thesis: for mk being Element of SCM-Data-Loc

for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let mk be Element of SCM-Data-Loc ; :: thesis: for r being Integer st x = [I,{},<*mk,r*>] holds

( x P21address = mk & x P22const = r )

let r be Integer; :: thesis: ( x = [I,{},<*mk,r*>] implies ( x P21address = mk & x P22const = r ) )

r in INT by INT_1:def 2;

then A1: ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;

assume A2: x = [I,{},<*mk,r*>] ; :: thesis: ( x P21address = mk & x P22const = r )

then consider f being FinSequence of SCM-Data-Loc \/ INT such that

A3: f = x `3_3 and

A4: x P21address = f /. 1 by Def4;

f = <*mk,r*> by A2, A3;

hence x P21address = mk by A4, A1, FINSEQ_4:17; :: thesis: x P22const = r

consider f being FinSequence of SCM-Data-Loc \/ INT such that

A5: f = x `3_3 and

A6: x P22const = f /. 2 by A2, Def5;

f = <*mk,r*> by A2, A5;

hence x P22const = r by A1, A6, FINSEQ_4:17; :: thesis: verum