let k1 be natural number ; :: thesis: (product" (AddressParts (InsCode (SCM-goto k1)))) . 1 = NAT
dom (product" (AddressParts (InsCode (SCM-goto k1)))) = {1} by Th22, MCART_1:7;
then A1: 1 in dom (product" (AddressParts (InsCode (SCM-goto k1)))) by TARSKI:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: NAT c= (product" (AddressParts (InsCode (SCM-goto k1)))) . 1

let x be set ; :: thesis: ( x in (product" (AddressParts (InsCode (SCM-goto k1)))) . 1 implies x in NAT )
assume x in (product" (AddressParts (InsCode (SCM-goto k1)))) . 1 ; :: thesis: x in NAT
then x in pi (AddressParts (InsCode (SCM-goto k1))),1 by A1, CARD_3:93;
then consider g being Function such that
A2: g in AddressParts (InsCode (SCM-goto k1)) and
A3: x = g . 1 by CARD_3:def 6;
consider I being Instruction of SCM such that
A4: g = AddressPart I and
A5: InsCode I = InsCode (SCM-goto k1) by A2;
consider i2 being Element of NAT such that
A6: I = SCM-goto i2 by A5, AMI_5:52, MCART_1:7;
g = <*i2*> by A4, A6, MCART_1:def 2;
then x = i2 by A3, FINSEQ_1:def 8;
hence x in NAT ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in (product" (AddressParts (InsCode (SCM-goto k1)))) . 1 )
assume x in NAT ; :: thesis: x in (product" (AddressParts (InsCode (SCM-goto k1)))) . 1
then reconsider x = x as Element of NAT ;
InsCode (SCM-goto k1) = 6 by MCART_1:7;
then ( AddressPart (SCM-goto x) = <*x*> & InsCode (SCM-goto k1) = InsCode (SCM-goto x) ) by MCART_1:7;
then A7: <*x*> in AddressParts (InsCode (SCM-goto k1)) ;
<*x*> . 1 = x by FINSEQ_1:def 8;
then x in pi (AddressParts (InsCode (SCM-goto k1))),1 by A7, CARD_3:def 6;
hence x in (product" (AddressParts (InsCode (SCM-goto k1)))) . 1 by A1, CARD_3:93; :: thesis: verum