let a, b be Data-Location ; :: thesis: (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 = SCM-Data-Loc
dom (product" (AddressParts (InsCode (SubFrom a,b)))) = {1,2} by Th19, MCART_1:7;
then A1: 1 in dom (product" (AddressParts (InsCode (SubFrom a,b)))) by TARSKI:def 2;

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

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 implies x in SCM-Data-Loc )
assume x in (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 ; :: thesis: x in SCM-Data-Loc
then x in pi (AddressParts (InsCode (SubFrom a,b))),1 by A1, CARD_3:def 13;
then consider f being Function such that
A2: f in AddressParts (InsCode (SubFrom a,b)) and
A3: f . 1 = x by CARD_3:def 6;
consider I being Instruction of SCM such that
A4: f = AddressPart I and
A5: InsCode I = InsCode (SubFrom a,b) by A2;
consider d1, d2 being Data-Location such that
A6: I = SubFrom d1,d2 by A5, AMI_5:49, MCART_1:7;
x = <*d1,d2*> . 1 by A3, A4, A6, MCART_1:def 2
.= d1 by FINSEQ_1:61 ;
hence x in SCM-Data-Loc by AMI_3:def 2; :: 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 (SubFrom a,b)))) . 1 )
assume x in SCM-Data-Loc ; :: thesis: x in (product" (AddressParts (InsCode (SubFrom a,b)))) . 1
then reconsider x = x as Data-Location by AMI_3:def 2;
( InsCode (SubFrom a,b) = 3 & InsCode (SubFrom x,b) = 3 ) by MCART_1:7;
then AddressPart (SubFrom x,b) in AddressParts (InsCode (SubFrom a,b)) ;
then A7: (AddressPart (SubFrom x,b)) . 1 in pi (AddressParts (InsCode (SubFrom a,b))),1 by CARD_3:def 6;
(AddressPart (SubFrom x,b)) . 1 = <*x,b*> . 1 by MCART_1:def 2
.= x by FINSEQ_1:61 ;
hence x in (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 by A1, A7, CARD_3:def 13; :: thesis: verum