JumpPart I is NAT -valued

proof

let x be set ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not x in proj2 (JumpPart I) or x in NAT )
assume x in rng (JumpPart I) ; :: thesis: x in NAT
then consider k being set such that
W1: k in dom (JumpPart I) and
W2: (JumpPart I) . k = x by FUNCT_1:def 5;
set X = JumpParts (InsCode I);
A: JumpPart I in JumpParts (InsCode I) ;
then k in dom (product" (JumpParts (InsCode I))) by W1, CARD_3:150;
then (JumpPart I) . k in (product" (JumpParts (InsCode I))) . k by A, CARD_3:151;
hence x in NAT by W1, W2, Def11; :: thesis: verum

end;

hence for b₁ being Function st b₁ = JumpPart I holds
b₁ is NAT -valued ; :: thesis: verum