let R be good Ring; :: thesis: for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
let i1 be Element of NAT ; :: thesis: (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
dom (product" (JumpParts (InsCode (goto (i1,R))))) = {1} by Th14, Th38;
then A1: 1 in dom (product" (JumpParts (InsCode (goto (i1,R))))) by TARSKI:def 1;
A2: InsCode (goto (i1,R)) = 6 by RECDEF_2:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: NAT c= (product" (JumpParts (InsCode (goto (i1,R))))) . 1

let x be set ; :: thesis: ( x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 ; :: thesis: x in NAT
then x in pi ((JumpParts (InsCode (goto (i1,R)))),1) by A1, CARD_3:76;
then consider g being Function such that
A3: g in JumpParts (InsCode (goto (i1,R))) and
A4: x = g . 1 by CARD_3:def 6;
consider I being Instruction of (SCM R) such that
A5: g = JumpPart I and
A6: InsCode I = InsCode (goto (i1,R)) by A3;
consider i2 being Element of NAT such that
A7: I = goto (i2,R) by A2, A6, Th22;
g = <*i2*> by A5, A7, RECDEF_2:def 2;
then x = i2 by A4, 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" (JumpParts (InsCode (goto (i1,R))))) . 1 )
assume x in NAT ; :: thesis: x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1
then reconsider x = x as Element of NAT ;
( JumpPart (goto (x,R)) = <*x*> & InsCode (goto (i1,R)) = InsCode (goto (x,R)) ) by A2, RECDEF_2:def 1, RECDEF_2:def 2;
then A8: <*x*> in JumpParts (InsCode (goto (i1,R))) ;
<*x*> . 1 = x by FINSEQ_1:def 8;
then x in pi ((JumpParts (InsCode (goto (i1,R)))),1) by A8, CARD_3:def 6;
hence x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 by A1, CARD_3:76; :: thesis: verum