let R be Ring; for i1 being Nat holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
let i1 be Nat; (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
dom (product" (JumpParts (InsCode (goto (i1,R))))) = {1}
by Th25;
then A1:
1 in dom (product" (JumpParts (InsCode (goto (i1,R)))))
by TARSKI:def 1;
hereby TARSKI:def 3,
XBOOLE_0:def 10 NAT c= (product" (JumpParts (InsCode (goto (i1,R))))) . 1
let x be
object ;
( x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 implies x in NAT )assume
x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1
;
x in NAT then
x in pi (
(JumpParts (InsCode (goto (i1,R)))),1)
by A1, CARD_3:def 12;
then consider g being
Function such that A2:
g in JumpParts (InsCode (goto (i1,R)))
and A3:
x = g . 1
by CARD_3:def 6;
consider I being
Instruction of
(SCM R) such that A4:
g = JumpPart I
and A5:
InsCode I = InsCode (goto (i1,R))
by A2;
consider i2 being
Nat such that A6:
I = goto (
i2,
R)
by A5, Th17;
g = <*i2*>
by A4, A6;
then
x = i2
by A3, FINSEQ_1:def 8;
hence
x in NAT
by ORDINAL1:def 12;
verum
end;
let x be object ; TARSKI:def 3 ( not x in NAT or x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1 )
assume
x in NAT
; 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)) )
;
then A7:
<*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 A7, CARD_3:def 6;
hence
x in (product" (JumpParts (InsCode (goto (i1,R))))) . 1
by A1, CARD_3:def 12; verum