let R be good Ring; :: thesis: for r being Element of R
for a being Data-Location of R holds (product" (AddressParts (InsCode (a := r)))) . 1 = SCM-Data-Loc
let r be Element of R; :: thesis: for a being Data-Location of R holds (product" (AddressParts (InsCode (a := r)))) . 1 = SCM-Data-Loc
let a be Data-Location of R; :: thesis: (product" (AddressParts (InsCode (a := r)))) . 1 = SCM-Data-Loc
A1: InsCode (a := r) = 5 by MCART_1:def 1;
dom (product" (AddressParts (InsCode (a := r)))) = {1,2} by Th13, Th37;
then A2: 1 in dom (product" (AddressParts (InsCode (a := r)))) by TARSKI:def 2;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: SCM-Data-Loc c= (product" (AddressParts (InsCode (a := r)))) . 1

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (a := r)))) . 1 implies x in SCM-Data-Loc )
assume x in (product" (AddressParts (InsCode (a := r)))) . 1 ; :: thesis: x in SCM-Data-Loc
then x in pi (AddressParts (InsCode (a := r))),1 by A2, CARD_3:def 13;
then consider f being Function such that
A3: f in AddressParts (InsCode (a := r)) and
A4: f . 1 = x by CARD_3:def 6;
consider I being Instruction of (SCM R) such that
A5: f = AddressPart I and
A6: InsCode I = InsCode (a := r) by A3;
InsCode I = 5 by A6, MCART_1:def 1;
then consider d1 being Data-Location of R, r2 being Element of R such that
A7: I = d1 := r2 by Th21;
x = <*d1,r2*> . 1 by A4, A5, A7, MCART_1:def 2
.= d1 by FINSEQ_1:61 ;
hence x in SCM-Data-Loc by SCMRING2:1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Data-Loc or x in (product" (AddressParts (InsCode (a := r)))) . 1 )
assume x in SCM-Data-Loc ; :: thesis: x in (product" (AddressParts (InsCode (a := r)))) . 1
then reconsider x = x as Data-Location of R by SCMRING2:1;
consider r1 being Element of R;
InsCode (x := r1) = 5 by MCART_1:def 1;
then AddressPart (x := r1) in AddressParts (InsCode (a := r)) by A1;
then A8: (AddressPart (x := r1)) . 1 in pi (AddressParts (InsCode (a := r))),1 by CARD_3:def 6;
(AddressPart (x := r1)) . 1 = <*x,r1*> . 1 by MCART_1:def 2
.= x by FINSEQ_1:61 ;
hence x in (product" (AddressParts (InsCode (a := r)))) . 1 by A2, A8, CARD_3:def 13; :: thesis: verum