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