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 ; :: thesis:
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: f = x `3_3 and
A6: x P22const = f /. 2 by ;
f = <*mk,r*> by A2, A5;
hence x P22const = r by ; :: thesis: verum