let R be good Ring; :: thesis: for a being Data-Location of R
for i1 being Instruction-Location of SCM R holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 = NAT
let a be Data-Location of R; :: thesis: for i1 being Instruction-Location of SCM R holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 = NAT
let i1 be Instruction-Location of SCM R; :: thesis: (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 = NAT
dom (product" (AddressParts (InsCode (a =0_goto i1)))) = {1,2} by Th15, Th39;
then A1: 1 in dom (product" (AddressParts (InsCode (a =0_goto i1)))) by TARSKI:def 2;
A2: InsCode (a =0_goto i1) = 7 by MCART_1:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: NAT c= (product" (AddressParts (InsCode (a =0_goto i1)))) . 1

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 implies x in NAT )
assume x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 ; :: thesis: x in NAT
then x in pi (AddressParts (InsCode (a =0_goto i1))),1 by A1, CARD_3:93;
then consider g being Function such that
A3: g in AddressParts (InsCode (a =0_goto i1)) and
A4: x = g . 1 by CARD_3:def 6;
consider I being Instruction of (SCM R) such that
A5: g = AddressPart I and
A6: InsCode I = InsCode (a =0_goto i1) by A3;
consider b being Data-Location of R, i2 being Instruction-Location of SCM R such that
A7: I = b =0_goto i2 by A2, A6, Th23;
g = <*i2,b*> by A5, A7, MCART_1:def 2;
then x = i2 by A4, FINSEQ_1:61;
hence x in NAT by AMI_1:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 )
assume x in NAT ; :: thesis: x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 1
then reconsider x = x as Instruction-Location of SCM R by AMI_1:def 4;
A8: AddressPart (a =0_goto x) = <*x,a*> by MCART_1:def 2;
InsCode (a =0_goto i1) = InsCode (a =0_goto x) by A2, MCART_1:def 1;
then A9: <*x,a*> in AddressParts (InsCode (a =0_goto i1)) by A8;
<*x,a*> . 1 = x by FINSEQ_1:61;
then x in pi (AddressParts (InsCode (a =0_goto i1))),1 by A9, CARD_3:def 6;
hence x in (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 by A1, CARD_3:93; :: thesis: verum