let a be Data-Location; :: thesis: for k1 being Nat holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT
let k1 be Nat; :: thesis: (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT
dom (product" (JumpParts (InsCode (a =0_goto k1)))) = {1} by Th10;
then A1: 1 in dom (product" (JumpParts (InsCode (a =0_goto k1)))) by TARSKI:def 1;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: NAT c= (product" (JumpParts (InsCode (a =0_goto k1)))) . 1
let x be object ; :: thesis: ( x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 implies x in NAT )
assume x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 ; :: thesis:
then x in pi ((JumpParts (InsCode (a =0_goto k1))),1) by ;
then consider g being Function such that
A2: g in JumpParts (InsCode (a =0_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 (a =0_goto k1) by A2;
InsCode I = 7 by A5;
then consider i2 being Nat, b being Data-Location such that
A6: I = b =0_goto i2 by AMI_5:14;
g = <*i2*> by A4, A6;
then x = i2 by ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 )
assume x in NAT ; :: thesis: x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1
then reconsider x = x as Element of NAT ;
( JumpPart (a =0_goto x) = <*x*> & InsCode (a =0_goto k1) = InsCode (a =0_goto x) ) ;
then A7: <*x*> in JumpParts (InsCode (a =0_goto k1)) ;
<*x*> . 1 = x by FINSEQ_1:40;
then x in pi ((JumpParts (InsCode (a =0_goto k1))),1) by ;
hence x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 by ; :: thesis: verum