let k1 be Nat; :: thesis: (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT

dom (product" (JumpParts (InsCode (SCM-goto k1)))) = {1} by Th9;

then A1: 1 in dom (product" (JumpParts (InsCode (SCM-goto k1)))) by TARSKI:def 1;

assume x in NAT ; :: thesis: x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1

then reconsider x = x as Element of NAT ;

( JumpPart (SCM-goto x) = <*x*> & InsCode (SCM-goto k1) = InsCode (SCM-goto x) ) ;

then A7: <*x*> in JumpParts (InsCode (SCM-goto k1)) ;

<*x*> . 1 = x by FINSEQ_1:def 8;

then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A7, CARD_3:def 6;

hence x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 by A1, CARD_3:def 12; :: thesis: verum

dom (product" (JumpParts (InsCode (SCM-goto k1)))) = {1} by Th9;

then A1: 1 in dom (product" (JumpParts (InsCode (SCM-goto k1)))) by TARSKI:def 1;

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 )let x be object ; :: thesis: ( x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 implies x in NAT )

assume x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 ; :: thesis: x in NAT

then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A1, CARD_3:def 12;

then consider g being Function such that

A2: g in JumpParts (InsCode (SCM-goto k1)) and

A3: x = g . 1 by CARD_3:def 6;

consider I being Instruction of SCM such that

A4: g = JumpPart I and

A5: InsCode I = InsCode (SCM-goto k1) by A2;

InsCode I = 6 by A5;

then consider i2 being Nat such that

A6: I = SCM-goto i2 by AMI_5:13;

g = <*i2*> by A4, A6;

then x = i2 by A3, FINSEQ_1:def 8;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 ; :: thesis: x in NAT

then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A1, CARD_3:def 12;

then consider g being Function such that

A2: g in JumpParts (InsCode (SCM-goto k1)) and

A3: x = g . 1 by CARD_3:def 6;

consider I being Instruction of SCM such that

A4: g = JumpPart I and

A5: InsCode I = InsCode (SCM-goto k1) by A2;

InsCode I = 6 by A5;

then consider i2 being Nat such that

A6: I = SCM-goto i2 by AMI_5:13;

g = <*i2*> by A4, A6;

then x = i2 by A3, FINSEQ_1:def 8;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

assume x in NAT ; :: thesis: x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1

then reconsider x = x as Element of NAT ;

( JumpPart (SCM-goto x) = <*x*> & InsCode (SCM-goto k1) = InsCode (SCM-goto x) ) ;

then A7: <*x*> in JumpParts (InsCode (SCM-goto k1)) ;

<*x*> . 1 = x by FINSEQ_1:def 8;

then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A7, CARD_3:def 6;

hence x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 by A1, CARD_3:def 12; :: thesis: verum