let i1 be Element of NAT ; :: thesis: for a being Int-Location holds (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 = SCM+FSA-Data-Loc
let a be Int-Location ; :: thesis: (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 = SCM+FSA-Data-Loc
A1: InsCode (a >0_goto i1) = 8 by SCMFSA_2:49;
dom (product" (AddressParts (InsCode (a >0_goto i1)))) = {1,2} by Th38, SCMFSA_2:49;
then A2: 2 in dom (product" (AddressParts (InsCode (a >0_goto i1)))) by TARSKI:def 2;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: SCM+FSA-Data-Loc c= (product" (AddressParts (InsCode (a >0_goto i1)))) . 2

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 implies x in SCM+FSA-Data-Loc )
assume x in (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 ; :: thesis: x in SCM+FSA-Data-Loc
then x in pi (AddressParts (InsCode (a >0_goto i1))),2 by A2, CARD_3:def 13;
then consider f being Function such that
A3: f in AddressParts (InsCode (a >0_goto i1)) and
A4: f . 2 = x by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A5: f = AddressPart I and
A6: InsCode I = InsCode (a >0_goto i1) by A3;
consider i2 being Element of NAT , b being Int-Location such that
A7: I = b >0_goto i2 by A6, SCMFSA_2:49, SCMFSA_2:61;
x = <*i2,b*> . 2 by A4, A5, A7, Th25
.= b by FINSEQ_1:61 ;
hence x in SCM+FSA-Data-Loc by SCMFSA_2:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM+FSA-Data-Loc or x in (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 )
assume x in SCM+FSA-Data-Loc ; :: thesis: x in (product" (AddressParts (InsCode (a >0_goto i1)))) . 2
then reconsider x = x as Int-Location by SCMFSA_2:28;
InsCode (x >0_goto i1) = 8 by SCMFSA_2:49;
then AddressPart (x >0_goto i1) in AddressParts (InsCode (a >0_goto i1)) by A1;
then A8: (AddressPart (x >0_goto i1)) . 2 in pi (AddressParts (InsCode (a >0_goto i1))),2 by CARD_3:def 6;
(AddressPart (x >0_goto i1)) . 2 = <*i1,x*> . 2 by Th25
.= x by FINSEQ_1:61 ;
hence x in (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 by A2, A8, CARD_3:def 13; :: thesis: verum