let I be Element of Segm 15; :: 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 ) )

A1: ( 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 A2: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;

k2 in INT by INT_1:def 2;

then A3: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;

assume A4: x = [I,{},<*d1,d2,k1,k2*>] ; :: thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )

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

A5: f = x `3_3 and

A6: x P41address = f /. 1 by Def9;

f = <*d1,d2,k1,k2*> by A4, A5;

hence x P41address = d1 by A1, A2, A3, A6, FINSEQ_4:80; :: thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 )

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

A7: f = x `3_3 and

A8: x P42address = f /. 2 by A4, Def10;

f = <*d1,d2,k1,k2*> by A4, A7;

hence x P42address = d2 by A1, A2, A3, A8, FINSEQ_4:80; :: thesis: ( x P43const = k1 & x P44const = k2 )

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

A9: f = x `3_3 and

A10: x P43const = f /. 3 by A4, Def11;

f = <*d1,d2,k1,k2*> by A4, A9;

hence x P43const = k1 by A1, A2, A3, A10, FINSEQ_4:80; :: thesis: x P44const = k2

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

A11: f = x `3_3 and

A12: x P44const = f /. 4 by A4, Def12;

f = <*d1,d2,k1,k2*> by A4, A11;

hence x P44const = k2 by A1, A2, A3, A12, FINSEQ_4:80; :: thesis: verum

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 ) )

A1: ( 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 A2: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;

k2 in INT by INT_1:def 2;

then A3: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def 3;

assume A4: x = [I,{},<*d1,d2,k1,k2*>] ; :: thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 )

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

A5: f = x `3_3 and

A6: x P41address = f /. 1 by Def9;

f = <*d1,d2,k1,k2*> by A4, A5;

hence x P41address = d1 by A1, A2, A3, A6, FINSEQ_4:80; :: thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 )

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

A7: f = x `3_3 and

A8: x P42address = f /. 2 by A4, Def10;

f = <*d1,d2,k1,k2*> by A4, A7;

hence x P42address = d2 by A1, A2, A3, A8, FINSEQ_4:80; :: thesis: ( x P43const = k1 & x P44const = k2 )

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

A9: f = x `3_3 and

A10: x P43const = f /. 3 by A4, Def11;

f = <*d1,d2,k1,k2*> by A4, A9;

hence x P43const = k1 by A1, A2, A3, A10, FINSEQ_4:80; :: thesis: x P44const = k2

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

A11: f = x `3_3 and

A12: x P44const = f /. 4 by A4, Def12;

f = <*d1,d2,k1,k2*> by A4, A11;

hence x P44const = k2 by A1, A2, A3, A12, FINSEQ_4:80; :: thesis: verum