let R be good Ring; :: thesis: for a being Data-Location of R
for i1 being Element of NAT holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM-Data-Loc
let a be Data-Location of R; :: thesis: for i1 being Element of NAT holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM-Data-Loc
let i1 be Element of NAT ; :: thesis: (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM-Data-Loc
dom (product" (AddressParts (InsCode (a =0_goto i1)))) = {1,2} by Th15, Th39;
then A1: 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-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-Data-Loc )
assume x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 ; :: thesis: x in SCM-Data-Loc
then x in pi (AddressParts (InsCode (a =0_goto i1))),2 by A1, CARD_3:def 13;
then consider f being Function such that
A2: f in AddressParts (InsCode (a =0_goto i1)) and
A3: f . 2 = x by CARD_3:def 6;
consider I being Instruction of (SCM R) such that
A4: f = AddressPart I and
A5: InsCode I = InsCode (a =0_goto i1) by A2;
InsCode I = 7 by A5, MCART_1:def 1;
then consider b being Data-Location of R, i2 being Element of NAT such that
A6: I = b =0_goto i2 by Th23;
x = <*i2,b*> . 2 by A3, A4, A6, MCART_1:def 2
.= b by FINSEQ_1:61 ;
hence x in SCM-Data-Loc by SCMRING2:1; :: thesis: verum

end;

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