let I be Element of Segm 14; :: thesis: for x being Element of SCMPDS-Instr
for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let x be Element of SCMPDS-Instr ; :: thesis: for d1, d2 being Element of SCM-Data-Loc
for k1, k2 being Integer st x = [I,<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let d1, d2 be Element of SCM-Data-Loc ; :: thesis: for k1, k2 being Integer st x = [I,<*d1,d2,k1,k2*>] holds
( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
let k1, k2 be Integer; :: thesis: ( x = [I,<*d1,d2,k1,k2*>] implies ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) )
assume A1: x = [I,<*d1,d2,k1,k2*>] ; :: thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )
A2: ( d1 is Element of SCM-Data-Loc \/ INT & d2 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def 3;
k1 in INT by INT_1:def 2;
then A3: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
k2 in INT by INT_1:def 2;
then A4: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A5: ( f = x `2 & x P41address = f /. 1 ) by A1, Def17;
f = <*d1,d2,k1,k2*> by A1, A5, MCART_1:7;
hence x P41address = d1 by A2, A3, A4, A5, FINSEQ_4:95; :: thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A6: ( f = x `2 & x P42address = f /. 2 ) by A1, Def18;
f = <*d1,d2,k1,k2*> by A1, A6, MCART_1:7;
hence x P42address = d2 by A2, A3, A4, A6, FINSEQ_4:95; :: thesis: ( x P43const = k1 & x P44const = k2 )
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A7: ( f = x `2 & x P43const = f /. 3 ) by A1, Def19;
f = <*d1,d2,k1,k2*> by A1, A7, MCART_1:7;
hence x P43const = k1 by A2, A3, A4, A7, FINSEQ_4:95; :: thesis: x P44const = k2
consider f being FinSequence of SCM-Data-Loc \/ INT such that
A8: ( f = x `2 & x P44const = f /. 4 ) by A1, Def20;
f = <*d1,d2,k1,k2*> by A1, A8, MCART_1:7;
hence x P44const = k2 by A2, A3, A4, A8, FINSEQ_4:95; :: thesis: verum